[Merged by Bors] - chore(Data/Int/Fib): add fib_neg

[themathqueen]

Forgot to add Int.fib_neg:

theorem fib_neg (n : ℤ) : fib (-n) = if Even n then -fib n else fib n := by

Also changes Int.fib_gcd to Int.gcd_fib and gets rid of the unnecessary coercions.

---

• depends on: [Merged by Bors] - chore: fix dependency counting script #32133

[github-actions]

PR summary 757fe2ec80

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Algebra.Ring.Parity	182	185	+3 (+1.65%)

Import changes for all files

Files	Import difference
860 files Mathlib.Algebra.Algebra.Basic Mathlib.Algebra.Algebra.Bilinear Mathlib.Algebra.Algebra.Defs Mathlib.Algebra.Algebra.Equiv Mathlib.Algebra.Algebra.Hom Mathlib.Algebra.Algebra.IsSimpleRing Mathlib.Algebra.Algebra.NonUnitalHom Mathlib.Algebra.Algebra.NonUnitalSubalgebra Mathlib.Algebra.Algebra.Opposite Mathlib.Algebra.Algebra.Pi Mathlib.Algebra.Algebra.Prod Mathlib.Algebra.Algebra.RestrictScalars Mathlib.Algebra.Algebra.Shrink Mathlib.Algebra.Algebra.Subalgebra.Basic Mathlib.Algebra.Algebra.Subalgebra.Matrix Mathlib.Algebra.Algebra.Subalgebra.Order Mathlib.Algebra.Algebra.Tower Mathlib.Algebra.Algebra.TransferInstance Mathlib.Algebra.BigOperators.Associated Mathlib.Algebra.BigOperators.Fin Mathlib.Algebra.BigOperators.Finprod Mathlib.Algebra.BigOperators.Finsupp.Basic Mathlib.Algebra.BigOperators.Finsupp.Fin Mathlib.Algebra.BigOperators.GroupWithZero.Action Mathlib.Algebra.BigOperators.Ring.Finset Mathlib.Algebra.BigOperators.Ring.Nat Mathlib.Algebra.BigOperators.WithTop Mathlib.Algebra.Category.BoolRing Mathlib.Algebra.Category.Grp.Adjunctions Mathlib.Algebra.Category.Grp.Basic Mathlib.Algebra.Category.Grp.Biproducts Mathlib.Algebra.Category.Grp.CartesianMonoidal Mathlib.Algebra.Category.Grp.ChosenFiniteProducts Mathlib.Algebra.Category.Grp.EpiMono Mathlib.Algebra.Category.Grp.EquivalenceGroupAddGroup Mathlib.Algebra.Category.Grp.FilteredColimits Mathlib.Algebra.Category.Grp.FiniteGrp Mathlib.Algebra.Category.Grp.ForgetCorepresentable Mathlib.Algebra.Category.Grp.Kernels Mathlib.Algebra.Category.Grp.LeftExactFunctor Mathlib.Algebra.Category.Grp.Limits Mathlib.Algebra.Category.Grp.Preadditive Mathlib.Algebra.Category.Grp.Subobject Mathlib.Algebra.Category.Grp.Yoneda Mathlib.Algebra.Category.Grp.ZModuleEquivalence Mathlib.Algebra.Category.Grp.Zero Mathlib.Algebra.Category.ModuleCat.Algebra Mathlib.Algebra.Category.ModuleCat.Basic Mathlib.Algebra.Category.ModuleCat.EpiMono Mathlib.Algebra.Category.ModuleCat.Injective Mathlib.Algebra.Category.ModuleCat.Kernels Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric Mathlib.Algebra.Category.ModuleCat.Semi Mathlib.Algebra.Category.ModuleCat.Subobject Mathlib.Algebra.Category.ModuleCat.Tannaka Mathlib.Algebra.Category.Ring.Basic Mathlib.Algebra.Category.Ring.Colimits Mathlib.Algebra.Category.Ring.FilteredColimits Mathlib.Algebra.Category.Ring.Limits Mathlib.Algebra.CharP.Invertible Mathlib.Algebra.CharZero.Quotient Mathlib.Algebra.ContinuedFractions.ContinuantsRecurrence Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv Mathlib.Algebra.ContinuedFractions.Determinant Mathlib.Algebra.ContinuedFractions.TerminatedStable Mathlib.Algebra.ContinuedFractions.Translations Mathlib.Algebra.DirectSum.AddChar Mathlib.Algebra.DirectSum.Basic Mathlib.Algebra.DirectSum.Ring Mathlib.Algebra.Exact Mathlib.Algebra.Field.GeomSum Mathlib.Algebra.Field.Opposite Mathlib.Algebra.Field.Subfield.Basic Mathlib.Algebra.FiveLemma Mathlib.Algebra.FreeAbelianGroup.Finsupp Mathlib.Algebra.FreeAbelianGroup.UniqueSums Mathlib.Algebra.GeomSum Mathlib.Algebra.Group.AddChar Mathlib.Algebra.Group.ConjFinite Mathlib.Algebra.Group.PNatPowAssoc Mathlib.Algebra.Group.Pointwise.Set.Card Mathlib.Algebra.Group.Subgroup.Finite Mathlib.Algebra.Group.Subgroup.Finsupp Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas Mathlib.Algebra.Group.Submonoid.Finsupp Mathlib.Algebra.GroupWithZero.Pointwise.Set.Card Mathlib.Algebra.GroupWithZero.Torsion Mathlib.Algebra.Homology.Additive Mathlib.Algebra.Homology.AlternatingConst Mathlib.Algebra.Homology.Augment Mathlib.Algebra.Homology.CommSq Mathlib.Algebra.Homology.DifferentialObject Mathlib.Algebra.Homology.Double Mathlib.Algebra.Homology.Embedding.AreComplementary Mathlib.Algebra.Homology.Embedding.Boundary Mathlib.Algebra.Homology.Embedding.Connect Mathlib.Algebra.Homology.Embedding.ExtendHomology Mathlib.Algebra.Homology.Embedding.Extend Mathlib.Algebra.Homology.Embedding.HomEquiv Mathlib.Algebra.Homology.Embedding.IsSupported Mathlib.Algebra.Homology.Embedding.RestrictionHomology Mathlib.Algebra.Homology.Embedding.Restriction Mathlib.Algebra.Homology.Embedding.StupidTrunc Mathlib.Algebra.Homology.Embedding.TruncGEHomology Mathlib.Algebra.Homology.Embedding.TruncGE Mathlib.Algebra.Homology.Embedding.TruncLEHomology Mathlib.Algebra.Homology.Embedding.TruncLE Mathlib.Algebra.Homology.ExactSequence Mathlib.Algebra.Homology.Factorizations.Basic Mathlib.Algebra.Homology.Functor Mathlib.Algebra.Homology.GrothendieckAbelian Mathlib.Algebra.Homology.HomologicalBicomplex Mathlib.Algebra.Homology.HomologicalComplexAbelian Mathlib.Algebra.Homology.HomologicalComplexBiprod Mathlib.Algebra.Homology.HomologicalComplexLimits Mathlib.Algebra.Homology.HomologicalComplex Mathlib.Algebra.Homology.HomologySequenceLemmas Mathlib.Algebra.Homology.HomologySequence Mathlib.Algebra.Homology.HomotopyCategory Mathlib.Algebra.Homology.HomotopyCofiber Mathlib.Algebra.Homology.Homotopy Mathlib.Algebra.Homology.ImageToKernel Mathlib.Algebra.Homology.LeftResolution.Basic Mathlib.Algebra.Homology.LeftResolution.Reduced Mathlib.Algebra.Homology.LeftResolution.Transport Mathlib.Algebra.Homology.Linear Mathlib.Algebra.Homology.Localization Mathlib.Algebra.Homology.Opposite Mathlib.Algebra.Homology.QuasiIso Mathlib.Algebra.Homology.Refinements Mathlib.Algebra.Homology.ShortComplex.Abelian Mathlib.Algebra.Homology.ShortComplex.ExactFunctor Mathlib.Algebra.Homology.ShortComplex.Exact Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex Mathlib.Algebra.Homology.ShortComplex.Linear Mathlib.Algebra.Homology.ShortComplex.Preadditive Mathlib.Algebra.Homology.ShortComplex.ShortExact Mathlib.Algebra.Homology.ShortComplex.SnakeLemma Mathlib.Algebra.Homology.SingleHomology Mathlib.Algebra.Homology.Single Mathlib.Algebra.Homology.Square Mathlib.Algebra.IsPrimePow Mathlib.Algebra.Lie.Basic Mathlib.Algebra.Lie.NonUnitalNonAssocAlgebra Mathlib.Algebra.ModEq Mathlib.Algebra.Module.Basic Mathlib.Algebra.Module.BigOperators Mathlib.Algebra.Module.Card Mathlib.Algebra.Module.Congruence.Defs Mathlib.Algebra.Module.End Mathlib.Algebra.Module.Equiv.Basic Mathlib.Algebra.Module.Equiv.Defs Mathlib.Algebra.Module.Equiv.Opposite Mathlib.Algebra.Module.Hom Mathlib.Algebra.Module.Injective Mathlib.Algebra.Module.LinearMap.Basic Mathlib.Algebra.Module.LinearMap.Defs Mathlib.Algebra.Module.LinearMap.DivisionRing Mathlib.Algebra.Module.LinearMap.End Mathlib.Algebra.Module.LinearMap.Prod Mathlib.Algebra.Module.LinearMap.Rat Mathlib.Algebra.Module.LinearMap.Star Mathlib.Algebra.Module.LocalizedModule.AtPrime Mathlib.Algebra.Module.LocalizedModule.Away Mathlib.Algebra.Module.LocalizedModule.Basic Mathlib.Algebra.Module.LocalizedModule.Exact Mathlib.Algebra.Module.LocalizedModule.IsLocalization Mathlib.Algebra.Module.NatInt Mathlib.Algebra.Module.Rat Mathlib.Algebra.Module.Shrink Mathlib.Algebra.Module.SnakeLemma Mathlib.Algebra.Module.Submodule.Bilinear Mathlib.Algebra.Module.Submodule.EqLocus Mathlib.Algebra.Module.Submodule.Equiv Mathlib.Algebra.Module.Submodule.Invariant Mathlib.Algebra.Module.Submodule.IterateMapComap Mathlib.Algebra.Module.Submodule.Ker Mathlib.Algebra.Module.Submodule.Lattice Mathlib.Algebra.Module.Submodule.LinearMap Mathlib.Algebra.Module.Submodule.Map Mathlib.Algebra.Module.Submodule.Range Mathlib.Algebra.Module.Submodule.RestrictScalars Mathlib.Algebra.Module.Submodule.Union Mathlib.Algebra.Module.Torsion.Field Mathlib.Algebra.Module.Torsion.Free Mathlib.Algebra.Module.Torsion.Pi Mathlib.Algebra.Module.Torsion.Prod Mathlib.Algebra.Module.TransferInstance Mathlib.Algebra.Module.ULift Mathlib.Algebra.NoZeroSMulDivisors.Basic Mathlib.Algebra.NonAssoc.LieAdmissible.Defs Mathlib.Algebra.Order.Algebra Mathlib.Algebra.Order.Antidiag.Finsupp Mathlib.Algebra.Order.Antidiag.Pi Mathlib.Algebra.Order.Field.Canonical Mathlib.Algebra.Order.Field.GeomSum Mathlib.Algebra.Order.Field.Rat Mathlib.Algebra.Order.Floor.Div Mathlib.Algebra.Order.Interval.Basic Mathlib.Algebra.Order.Invertible Mathlib.Algebra.Order.Module.Algebra Mathlib.Algebra.Order.Module.Basic Mathlib.Algebra.Order.Module.Defs Mathlib.Algebra.Order.Module.Equiv Mathlib.Algebra.Order.Module.Field Mathlib.Algebra.Order.Module.OrderedSMul Mathlib.Algebra.Order.Module.Pointwise Mathlib.Algebra.Order.Module.PositiveLinearMap Mathlib.Algebra.Order.Monoid.PNat Mathlib.Algebra.Order.Monovary Mathlib.Algebra.Order.Nonneg.Field Mathlib.Algebra.Order.Nonneg.Module Mathlib.Algebra.Order.Rearrangement Mathlib.Algebra.Order.Ring.Finset Mathlib.Algebra.Order.Ring.GeomSum Mathlib.Algebra.Order.Ring.IsNonarchimedean Mathlib.Algebra.Order.Ring.Nat Mathlib.Algebra.Order.Ring.Ordering.Basic Mathlib.Algebra.Order.Ring.Ordering.Defs Mathlib.Algebra.Order.Ring.Pow Mathlib.Algebra.Order.Ring.Units Mathlib.Algebra.Ring.Center Mathlib.Algebra.Ring.CentroidHom Mathlib.Algebra.Ring.Divisibility.Lemmas Mathlib.Algebra.Ring.GeomSum Mathlib.Algebra.Ring.Semireal.Defs Mathlib.Algebra.Ring.Subring.Basic Mathlib.Algebra.Ring.Subring.MulOpposite Mathlib.Algebra.Ring.Subring.Pointwise Mathlib.Algebra.Ring.Subsemiring.Basic Mathlib.Algebra.Ring.Subsemiring.MulOpposite Mathlib.Algebra.Ring.Subsemiring.Pointwise Mathlib.Algebra.Ring.SumsOfSquares Mathlib.Algebra.RingQuot Mathlib.Algebra.Squarefree.Basic Mathlib.Algebra.Star.Basic Mathlib.Algebra.Star.Center Mathlib.Algebra.Star.CentroidHom Mathlib.Algebra.Star.Conjneg Mathlib.Algebra.Star.MonoidHom Mathlib.Algebra.Star.NonUnitalSubsemiring Mathlib.Algebra.Star.Pi Mathlib.Algebra.Star.Pointwise Mathlib.Algebra.Star.Prod Mathlib.Algebra.Star.RingQuot Mathlib.Algebra.Star.StarAlgHom Mathlib.Algebra.Star.StarRingHom Mathlib.Algebra.Star.Subsemiring Mathlib.AlgebraicTopology.AlternatingFaceMapComplex Mathlib.AlgebraicTopology.DoldKan.Decomposition Mathlib.AlgebraicTopology.DoldKan.Degeneracies Mathlib.AlgebraicTopology.DoldKan.EquivalenceAdditive Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian Mathlib.AlgebraicTopology.DoldKan.Equivalence Mathlib.AlgebraicTopology.DoldKan.Faces Mathlib.AlgebraicTopology.DoldKan.FunctorGamma Mathlib.AlgebraicTopology.DoldKan.FunctorN Mathlib.AlgebraicTopology.DoldKan.GammaCompN Mathlib.AlgebraicTopology.DoldKan.Homotopies Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence Mathlib.AlgebraicTopology.DoldKan.NCompGamma Mathlib.AlgebraicTopology.DoldKan.NReflectsIso Mathlib.AlgebraicTopology.DoldKan.Normalized Mathlib.AlgebraicTopology.DoldKan.Notations Mathlib.AlgebraicTopology.DoldKan.PInfty Mathlib.AlgebraicTopology.DoldKan.Projections Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject Mathlib.AlgebraicTopology.ExtraDegeneracy Mathlib.AlgebraicTopology.MooreComplex Mathlib.Analysis.Fourier.Notation Mathlib.CategoryTheory.Abelian.Basic Mathlib.CategoryTheory.Abelian.CommSq Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel Mathlib.CategoryTheory.Abelian.Exact Mathlib.CategoryTheory.Abelian.FunctorCategory Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.FunctorCategory Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Indization Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Sheaf Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Types Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Coseparator Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Monomorphisms Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject Mathlib.CategoryTheory.Abelian.Indization Mathlib.CategoryTheory.Abelian.Injective.Resolution Mathlib.CategoryTheory.Abelian.LeftDerived Mathlib.CategoryTheory.Abelian.Monomorphisms Mathlib.CategoryTheory.Abelian.NonPreadditive Mathlib.CategoryTheory.Abelian.Opposite Mathlib.CategoryTheory.Abelian.Projective.Resolution Mathlib.CategoryTheory.Abelian.Pseudoelements Mathlib.CategoryTheory.Abelian.Refinements Mathlib.CategoryTheory.Abelian.RightDerived Mathlib.CategoryTheory.Abelian.SerreClass.Basic Mathlib.CategoryTheory.Abelian.SerreClass.Bousfield Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty Mathlib.CategoryTheory.Abelian.Subobject Mathlib.CategoryTheory.Abelian.Transfer Mathlib.CategoryTheory.Action.Basic Mathlib.CategoryTheory.Action.Concrete Mathlib.CategoryTheory.Action.Continuous Mathlib.CategoryTheory.Action.Limits Mathlib.CategoryTheory.Action.Monoidal Mathlib.CategoryTheory.Action Mathlib.CategoryTheory.Adjunction.Additive Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems Mathlib.CategoryTheory.Center.Linear Mathlib.CategoryTheory.Center.Localization Mathlib.CategoryTheory.Center.Preadditive Mathlib.CategoryTheory.Comma.CardinalArrow Mathlib.CategoryTheory.Dialectica.Monoidal Mathlib.CategoryTheory.Distributive.Cartesian Mathlib.CategoryTheory.Distributive.Monoidal Mathlib.CategoryTheory.ExtremalEpi Mathlib.CategoryTheory.Functor.KanExtension.Dense Mathlib.CategoryTheory.Galois.Action Mathlib.CategoryTheory.Galois.Basic Mathlib.CategoryTheory.Galois.Decomposition Mathlib.CategoryTheory.Galois.Examples Mathlib.CategoryTheory.Galois.Full Mathlib.CategoryTheory.Galois.GaloisObjects Mathlib.CategoryTheory.Galois.Prorepresentability Mathlib.CategoryTheory.Generator.Abelian Mathlib.CategoryTheory.Generator.Basic Mathlib.CategoryTheory.Generator.HomologicalComplex Mathlib.CategoryTheory.Generator.Indization Mathlib.CategoryTheory.Generator.Preadditive Mathlib.CategoryTheory.Generator.Presheaf Mathlib.CategoryTheory.Generator.Sheaf Mathlib.CategoryTheory.Generator.StrongGenerator Mathlib.CategoryTheory.Idempotents.Basic Mathlib.CategoryTheory.Idempotents.Biproducts Mathlib.CategoryTheory.Idempotents.FunctorCategories Mathlib.CategoryTheory.Idempotents.FunctorExtension Mathlib.CategoryTheory.Idempotents.HomologicalComplex Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi Mathlib.CategoryTheory.Idempotents.Karoubi Mathlib.CategoryTheory.Idempotents.SimplicialObject Mathlib.CategoryTheory.Limits.ConcreteCategory.WithAlgebraicStructures Mathlib.CategoryTheory.Limits.SmallComplete Mathlib.CategoryTheory.Linear.Basic Mathlib.CategoryTheory.Linear.FunctorCategory Mathlib.CategoryTheory.Linear.LinearFunctor Mathlib.CategoryTheory.Linear.Yoneda Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive Mathlib.CategoryTheory.Localization.Linear Mathlib.CategoryTheory.Localization.Preadditive Mathlib.CategoryTheory.Localization.SmallShiftedHom Mathlib.CategoryTheory.Monoidal.Cartesian.CommGrp_ Mathlib.CategoryTheory.Monoidal.Cartesian.Grp_ Mathlib.CategoryTheory.Monoidal.Internal.Types.CommGrp_ Mathlib.CategoryTheory.Monoidal.Internal.Types.Grp_ Mathlib.CategoryTheory.Monoidal.Linear Mathlib.CategoryTheory.Monoidal.Preadditive Mathlib.CategoryTheory.Monoidal.Subcategory Mathlib.CategoryTheory.Monoidal.Tor Mathlib.CategoryTheory.MorphismProperty.HasCardinalLT Mathlib.CategoryTheory.MorphismProperty.Ind Mathlib.CategoryTheory.Noetherian Mathlib.CategoryTheory.ObjectProperty.ColimitsCardinalClosure Mathlib.CategoryTheory.ObjectProperty.ColimitsClosure Mathlib.CategoryTheory.ObjectProperty.EpiMono Mathlib.CategoryTheory.ObjectProperty.Extensions Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits Mathlib.CategoryTheory.ObjectProperty.HasCardinalLT Mathlib.CategoryTheory.ObjectProperty.Ind Mathlib.CategoryTheory.ObjectProperty.LimitsClosure Mathlib.CategoryTheory.Preadditive.AdditiveFunctor Mathlib.CategoryTheory.Preadditive.Basic Mathlib.CategoryTheory.Preadditive.Biproducts Mathlib.CategoryTheory.Preadditive.CommGrp_ Mathlib.CategoryTheory.Preadditive.EilenbergMoore Mathlib.CategoryTheory.Preadditive.EndoFunctor Mathlib.CategoryTheory.Preadditive.FunctorCategory Mathlib.CategoryTheory.Preadditive.Indization Mathlib.CategoryTheory.Preadditive.Injective.Resolution Mathlib.CategoryTheory.Preadditive.LeftExact Mathlib.CategoryTheory.Preadditive.LiftToFinset Mathlib.CategoryTheory.Preadditive.Mat Mathlib.CategoryTheory.Preadditive.Opposite Mathlib.CategoryTheory.Preadditive.Projective.Resolution Mathlib.CategoryTheory.Preadditive.SingleObj Mathlib.CategoryTheory.Preadditive.Transfer Mathlib.CategoryTheory.Preadditive.Yoneda.Basic Mathlib.CategoryTheory.Preadditive.Yoneda.Injective Mathlib.CategoryTheory.Preadditive.Yoneda.Projective Mathlib.CategoryTheory.Presentable.Adjunction Mathlib.CategoryTheory.Presentable.Basic Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation Mathlib.CategoryTheory.Presentable.ColimitPresentation Mathlib.CategoryTheory.Presentable.Dense Mathlib.CategoryTheory.Presentable.Finite Mathlib.CategoryTheory.Presentable.IsCardinalFiltered Mathlib.CategoryTheory.Presentable.Limits Mathlib.CategoryTheory.Presentable.LocallyPresentable Mathlib.CategoryTheory.Presentable.OrthogonalReflection Mathlib.CategoryTheory.Presentable.Retracts Mathlib.CategoryTheory.Presentable.Type Mathlib.CategoryTheory.Quotient.Linear Mathlib.CategoryTheory.Quotient.Preadditive Mathlib.CategoryTheory.Shift.InducedShiftSequence Mathlib.CategoryTheory.Shift.Linear Mathlib.CategoryTheory.Shift.Opposite Mathlib.CategoryTheory.Shift.Pullback Mathlib.CategoryTheory.Shift.ShiftSequence Mathlib.CategoryTheory.Shift.ShiftedHomOpposite Mathlib.CategoryTheory.Shift.ShiftedHom Mathlib.CategoryTheory.Simple Mathlib.CategoryTheory.Sites.Abelian Mathlib.CategoryTheory.Sites.Adjunction Mathlib.CategoryTheory.Sites.Canonical Mathlib.CategoryTheory.Sites.CartesianClosed Mathlib.CategoryTheory.Sites.CartesianMonoidal Mathlib.CategoryTheory.Sites.ChosenFiniteProducts Mathlib.CategoryTheory.Sites.Coherent.Basic Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology Mathlib.CategoryTheory.Sites.Coherent.Comparison Mathlib.CategoryTheory.Sites.Coherent.Equivalence Mathlib.CategoryTheory.Sites.Coherent.ExtensiveColimits Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective Mathlib.CategoryTheory.Sites.Coherent.ReflectsPrecoherent Mathlib.CategoryTheory.Sites.Coherent.ReflectsPreregular Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves Mathlib.CategoryTheory.Sites.Coherent.RegularTopology Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit Mathlib.CategoryTheory.Sites.Coherent.SheafComparison Mathlib.CategoryTheory.Sites.CompatiblePlus Mathlib.CategoryTheory.Sites.CompatibleSheafification Mathlib.CategoryTheory.Sites.ConcreteSheafification Mathlib.CategoryTheory.Sites.ConstantSheaf Mathlib.CategoryTheory.Sites.Continuous Mathlib.CategoryTheory.Sites.CoverLifting Mathlib.CategoryTheory.Sites.CoverPreserving Mathlib.CategoryTheory.Sites.Coverage Mathlib.CategoryTheory.Sites.CoversTop Mathlib.CategoryTheory.Sites.DenseSubsite.Basic Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv Mathlib.CategoryTheory.Sites.Descent.DescentData Mathlib.CategoryTheory.Sites.Descent.IsPrestack Mathlib.CategoryTheory.Sites.EpiMono Mathlib.CategoryTheory.Sites.Equivalence Mathlib.CategoryTheory.Sites.GlobalSections Mathlib.CategoryTheory.Sites.Hypercover.Homotopy Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf Mathlib.CategoryTheory.Sites.Hypercover.One Mathlib.CategoryTheory.Sites.LeftExact Mathlib.CategoryTheory.Sites.Limits Mathlib.CategoryTheory.Sites.Localization Mathlib.CategoryTheory.Sites.LocallyBijective Mathlib.CategoryTheory.Sites.LocallyFullyFaithful Mathlib.CategoryTheory.Sites.LocallyInjective Mathlib.CategoryTheory.Sites.LocallySurjective Mathlib.CategoryTheory.Sites.Monoidal Mathlib.CategoryTheory.Sites.MorphismProperty Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1 Mathlib.CategoryTheory.Sites.Over Mathlib.CategoryTheory.Sites.Plus Mathlib.CategoryTheory.Sites.Point.Basic Mathlib.CategoryTheory.Sites.PreservesLocallyBijective Mathlib.CategoryTheory.Sites.PreservesSheafification Mathlib.CategoryTheory.Sites.PseudofunctorSheafOver Mathlib.CategoryTheory.Sites.Pullback Mathlib.CategoryTheory.Sites.SheafHom Mathlib.CategoryTheory.Sites.Sheaf Mathlib.CategoryTheory.Sites.Sheafification Mathlib.CategoryTheory.Sites.Subcanonical Mathlib.CategoryTheory.Sites.Subsheaf Mathlib.CategoryTheory.Sites.Types Mathlib.CategoryTheory.Sites.Whiskering Mathlib.CategoryTheory.SmallObject.Basic Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument Mathlib.CategoryTheory.SmallRepresentatives Mathlib.CategoryTheory.Subobject.ArtinianObject Mathlib.CategoryTheory.Subobject.FactorThru Mathlib.CategoryTheory.Subobject.HasCardinalLT Mathlib.CategoryTheory.Subobject.Lattice Mathlib.CategoryTheory.Subobject.Limits Mathlib.CategoryTheory.Subobject.NoetherianObject Mathlib.CategoryTheory.Triangulated.Basic Mathlib.CategoryTheory.Triangulated.Opposite.Basic Mathlib.CategoryTheory.Triangulated.Opposite.Triangle Mathlib.CategoryTheory.Triangulated.Rotate Mathlib.Combinatorics.Additive.AP.Three.Defs Mathlib.Combinatorics.Additive.Corner.Defs Mathlib.Combinatorics.Additive.FreimanHom Mathlib.Combinatorics.Additive.PluenneckeRuzsa Mathlib.Combinatorics.Colex Mathlib.Combinatorics.Enumerative.Catalan Mathlib.Combinatorics.Enumerative.Composition Mathlib.Combinatorics.Enumerative.DoubleCounting Mathlib.Combinatorics.Enumerative.DyckWord Mathlib.Combinatorics.Enumerative.IncidenceAlgebra Mathlib.Combinatorics.Enumerative.InclusionExclusion Mathlib.Combinatorics.Enumerative.Partition.Basic Mathlib.Combinatorics.Enumerative.Partition Mathlib.Combinatorics.Matroid.Basic Mathlib.Combinatorics.Matroid.Circuit Mathlib.Combinatorics.Matroid.Closure Mathlib.Combinatorics.Matroid.Constructions Mathlib.Combinatorics.Matroid.Dual Mathlib.Combinatorics.Matroid.IndepAxioms Mathlib.Combinatorics.Matroid.Loop Mathlib.Combinatorics.Matroid.Map Mathlib.Combinatorics.Matroid.Minor.Contract Mathlib.Combinatorics.Matroid.Minor.Delete Mathlib.Combinatorics.Matroid.Minor.Order Mathlib.Combinatorics.Matroid.Minor.Restrict Mathlib.Combinatorics.Matroid.Rank.Cardinal Mathlib.Combinatorics.Matroid.Rank.ENat Mathlib.Combinatorics.Matroid.Rank.Finite Mathlib.Combinatorics.Matroid.Sum Mathlib.Combinatorics.Pigeonhole Mathlib.Combinatorics.SetFamily.FourFunctions Mathlib.Combinatorics.SetFamily.HarrisKleitman Mathlib.Combinatorics.SetFamily.Kleitman Mathlib.Combinatorics.SimpleGraph.Circulant Mathlib.Combinatorics.SimpleGraph.Clique Mathlib.Combinatorics.SimpleGraph.Coloring Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkCounting Mathlib.Combinatorics.SimpleGraph.Diam Mathlib.Combinatorics.SimpleGraph.Hasse Mathlib.Combinatorics.SimpleGraph.IncMatrix Mathlib.Combinatorics.SimpleGraph.Metric Mathlib.Combinatorics.SimpleGraph.Partition Mathlib.Combinatorics.SimpleGraph.Prod Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise Mathlib.Combinatorics.SimpleGraph.Sum Mathlib.Combinatorics.SimpleGraph.Trails Mathlib.Computability.Ackermann Mathlib.Computability.Encoding Mathlib.Computability.Halting Mathlib.Computability.PartrecCode Mathlib.Computability.Partrec Mathlib.Computability.Primrec Mathlib.Computability.Reduce Mathlib.Computability.TMConfig Mathlib.Computability.TMToPartrec Mathlib.Computability.TuringDegree Mathlib.Data.BitVec Mathlib.Data.DFinsupp.BigOperators Mathlib.Data.DFinsupp.Interval Mathlib.Data.DFinsupp.Lex Mathlib.Data.DFinsupp.Module Mathlib.Data.DFinsupp.Multiset Mathlib.Data.DFinsupp.Order Mathlib.Data.DFinsupp.Sigma Mathlib.Data.DFinsupp.Submonoid Mathlib.Data.DFinsupp.WellFounded Mathlib.Data.ENat.Basic Mathlib.Data.ENat.BigOperators Mathlib.Data.ENat.Lattice Mathlib.Data.ENat.Pow Mathlib.Data.Fin.Parity Mathlib.Data.Fin.Tuple.NatAntidiagonal Mathlib.Data.Fin.Tuple.Reflection Mathlib.Data.Finite.Card Mathlib.Data.Finite.Perm Mathlib.Data.Finset.Finsupp Mathlib.Data.Fintype.Units Mathlib.Data.Int.Bitwise Mathlib.Data.Int.Cast.Lemmas Mathlib.Data.Int.CharZero Mathlib.Data.Int.NatPrime Mathlib.Data.Matrix.Action Mathlib.Data.Matrix.Basic Mathlib.Data.Matrix.Basis Mathlib.Data.Matrix.Bilinear Mathlib.Data.Matrix.Composition Mathlib.Data.Matrix.Mul Mathlib.Data.Matrix.PEquiv Mathlib.Data.Multiset.Interval Mathlib.Data.Nat.BitIndices Mathlib.Data.Nat.Cast.Order.Ring Mathlib.Data.Nat.Choose.Sum Mathlib.Data.Nat.Factorial.NatCast Mathlib.Data.Nat.Factors Mathlib.Data.Nat.MaxPowDiv Mathlib.Data.Nat.PartENat Mathlib.Data.Nat.Prime.Int Mathlib.Data.Nat.PrimeFin Mathlib.Data.Num.Lemmas Mathlib.Data.Ordmap.Invariants Mathlib.Data.Ordmap.Ordset Mathlib.Data.PNat.Basic Mathlib.Data.PNat.Factors Mathlib.Data.PNat.Find Mathlib.Data.PNat.Order Mathlib.Data.PNat.Prime Mathlib.Data.PNat.Xgcd Mathlib.Data.Rat.Cardinal Mathlib.Data.Seq.Basic Mathlib.Data.Seq.Parallel Mathlib.Data.Seq.Seq Mathlib.Data.Seq.WSeq Mathlib.Data.Set.Card.Arithmetic Mathlib.Data.Set.Card Mathlib.Data.Setoid.Partition.Card Mathlib.Data.UInt Mathlib.Data.W.Cardinal Mathlib.Data.WSeq.Basic Mathlib.Data.WSeq.Defs Mathlib.Data.WSeq.Productive Mathlib.Data.WSeq.Relation Mathlib.Dynamics.BirkhoffSum.Average Mathlib.Dynamics.Flow Mathlib.Dynamics.Minimal Mathlib.Dynamics.OmegaLimit Mathlib.Dynamics.PeriodicPts.Lemmas Mathlib.Dynamics.Transitive Mathlib.FieldTheory.Galois.Notation Mathlib.Geometry.RingedSpace.Basic Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits Mathlib.Geometry.RingedSpace.SheafedSpace Mathlib.Geometry.RingedSpace.Stalks Mathlib.GroupTheory.Abelianization.Finite Mathlib.GroupTheory.ClassEquation Mathlib.GroupTheory.Commensurable Mathlib.GroupTheory.Commutator.Finite Mathlib.GroupTheory.Complement Mathlib.GroupTheory.CoprodI Mathlib.GroupTheory.Coset.Card Mathlib.GroupTheory.Divisible Mathlib.GroupTheory.FreeAbelianGroup Mathlib.GroupTheory.FreeGroup.NielsenSchreier Mathlib.GroupTheory.GroupAction.Blocks Mathlib.GroupTheory.GroupAction.CardCommute Mathlib.GroupTheory.GroupAction.Iwasawa Mathlib.GroupTheory.GroupAction.Primitive Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer Mathlib.GroupTheory.GroupExtension.Basic Mathlib.GroupTheory.GroupExtension.Defs Mathlib.GroupTheory.HNNExtension Mathlib.GroupTheory.IndexNormal Mathlib.GroupTheory.Index Mathlib.GroupTheory.MonoidLocalization.Cardinality Mathlib.GroupTheory.OreLocalization.Cardinality Mathlib.GroupTheory.Perm.DomMulAct Mathlib.GroupTheory.Perm.Subgroup Mathlib.GroupTheory.PushoutI Mathlib.GroupTheory.QuotientGroup.Basic Mathlib.GroupTheory.QuotientGroup.Finite Mathlib.GroupTheory.Rank Mathlib.GroupTheory.SemidirectProduct Mathlib.GroupTheory.Solvable Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs Mathlib.LinearAlgebra.BilinearForm.Basic Mathlib.LinearAlgebra.BilinearMap Mathlib.LinearAlgebra.Dual.Defs Mathlib.LinearAlgebra.GeneralLinearGroup Mathlib.LinearAlgebra.Goursat Mathlib.LinearAlgebra.Isomorphisms Mathlib.LinearAlgebra.LeftExact Mathlib.LinearAlgebra.LinearPMap Mathlib.LinearAlgebra.Matrix.Irreducible.Defs Mathlib.LinearAlgebra.Matrix.Orthogonal Mathlib.LinearAlgebra.Matrix.Unique Mathlib.LinearAlgebra.Multilinear.Basic Mathlib.LinearAlgebra.Multilinear.Curry Mathlib.LinearAlgebra.Multilinear.Pi Mathlib.LinearAlgebra.Multilinear.TensorProduct Mathlib.LinearAlgebra.PiTensorProduct Mathlib.LinearAlgebra.Pi Mathlib.LinearAlgebra.Prod Mathlib.LinearAlgebra.Projection Mathlib.LinearAlgebra.Quotient.Basic Mathlib.LinearAlgebra.Quotient.Card Mathlib.LinearAlgebra.Quotient.Defs Mathlib.LinearAlgebra.Quotient.Pi Mathlib.LinearAlgebra.Span.Basic Mathlib.LinearAlgebra.Span.Defs Mathlib.LinearAlgebra.TensorPower.Symmetric Mathlib.LinearAlgebra.TensorProduct.Associator Mathlib.LinearAlgebra.TensorProduct.Basic Mathlib.LinearAlgebra.TensorProduct.Pi Mathlib.LinearAlgebra.TensorProduct.Prod Mathlib.LinearAlgebra.TensorProduct.Tower Mathlib.MeasureTheory.Constructions.AddChar Mathlib.MeasureTheory.Constructions.SubmoduleQuotient Mathlib.MeasureTheory.MeasurableSpace.Card Mathlib.MeasureTheory.MeasurableSpace.NCard Mathlib.ModelTheory.Algebra.Field.Basic Mathlib.ModelTheory.Algebra.Ring.Basic Mathlib.ModelTheory.Arithmetic.Presburger.Basic Mathlib.ModelTheory.Basic Mathlib.ModelTheory.Bundled Mathlib.ModelTheory.Complexity Mathlib.ModelTheory.Definability Mathlib.ModelTheory.DirectLimit Mathlib.ModelTheory.ElementaryMaps Mathlib.ModelTheory.ElementarySubstructures Mathlib.ModelTheory.Encoding Mathlib.ModelTheory.Equivalence Mathlib.ModelTheory.FinitelyGenerated Mathlib.ModelTheory.Graph Mathlib.ModelTheory.LanguageMap Mathlib.ModelTheory.PartialEquiv Mathlib.ModelTheory.Quotients Mathlib.ModelTheory.Satisfiability Mathlib.ModelTheory.Semantics Mathlib.ModelTheory.Skolem Mathlib.ModelTheory.Substructures Mathlib.ModelTheory.Syntax Mathlib.ModelTheory.Types Mathlib.ModelTheory.Ultraproducts Mathlib.NumberTheory.ADEInequality Mathlib.NumberTheory.Basic Mathlib.NumberTheory.Padics.PadicVal.Defs Mathlib.Order.Extension.Well Mathlib.Order.Filter.AtTopBot.ModEq Mathlib.Order.Filter.CardinalInter Mathlib.Order.Filter.Cocardinal Mathlib.Order.Height Mathlib.Order.KrullDimension Mathlib.Order.Monotone.MonovaryOrder Mathlib.Order.Partition.Equipartition Mathlib.RingTheory.ChainOfDivisors Mathlib.RingTheory.Coprime.Lemmas Mathlib.RingTheory.Finiteness.Basic Mathlib.RingTheory.Finiteness.Bilinear Mathlib.RingTheory.Finiteness.Defs Mathlib.RingTheory.Finiteness.Lattice Mathlib.RingTheory.Finiteness.Prod Mathlib.RingTheory.FreeRing Mathlib.RingTheory.Ideal.Lattice Mathlib.RingTheory.Ideal.Maximal Mathlib.RingTheory.Ideal.Nonunits Mathlib.RingTheory.Ideal.Prime Mathlib.RingTheory.Ideal.Quotient.Defs Mathlib.RingTheory.Ideal.Span Mathlib.RingTheory.Invariant.Defs Mathlib.RingTheory.LocalRing.Basic Mathlib.RingTheory.LocalRing.MaximalIdeal.Defs Mathlib.RingTheory.LocalRing.Subring Mathlib.RingTheory.Localization.Basic Mathlib.RingTheory.Localization.Defs Mathlib.RingTheory.Localization.Integer Mathlib.RingTheory.Multiplicity Mathlib.RingTheory.Nilpotent.Basic Mathlib.RingTheory.Noetherian.Defs Mathlib.RingTheory.Noetherian.Filter Mathlib.RingTheory.NonUnitalSubring.Basic Mathlib.RingTheory.NonUnitalSubsemiring.Basic Mathlib.RingTheory.OreLocalization.Cardinality Mathlib.RingTheory.OreLocalization.Ring Mathlib.RingTheory.PiTensorProduct Mathlib.RingTheory.Radical Mathlib.RingTheory.SimpleRing.Congr Mathlib.RingTheory.SimpleRing.Field Mathlib.RingTheory.Spectrum.Maximal.Basic Mathlib.RingTheory.Spectrum.Maximal.Defs Mathlib.RingTheory.Spectrum.Prime.Defs Mathlib.RingTheory.TwoSidedIdeal.Operations Mathlib.RingTheory.UniqueFactorizationDomain.Basic Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet Mathlib.RingTheory.UniqueFactorizationDomain.Finite Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity Mathlib.RingTheory.UniqueFactorizationDomain.Nat Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors Mathlib.SetTheory.Cardinal.Aleph Mathlib.SetTheory.Cardinal.Arithmetic Mathlib.SetTheory.Cardinal.Basic Mathlib.SetTheory.Cardinal.Cofinality Mathlib.SetTheory.Cardinal.Continuum Mathlib.SetTheory.Cardinal.CountableCover Mathlib.SetTheory.Cardinal.Divisibility Mathlib.SetTheory.Cardinal.ENat Mathlib.SetTheory.Cardinal.Embedding Mathlib.SetTheory.Cardinal.Finite Mathlib.SetTheory.Cardinal.HasCardinalLT Mathlib.SetTheory.Cardinal.NatCount Mathlib.SetTheory.Cardinal.Order Mathlib.SetTheory.Cardinal.Ordinal Mathlib.SetTheory.Cardinal.Pigeonhole Mathlib.SetTheory.Cardinal.Regular Mathlib.SetTheory.Cardinal.Subfield Mathlib.SetTheory.Cardinal.ToNat Mathlib.SetTheory.Cardinal.UnivLE Mathlib.SetTheory.Game.Birthday Mathlib.SetTheory.Game.Domineering Mathlib.SetTheory.Game.Nim Mathlib.SetTheory.Game.Ordinal Mathlib.SetTheory.Game.Short Mathlib.SetTheory.Game.State Mathlib.SetTheory.Nimber.Basic Mathlib.SetTheory.Ordinal.Arithmetic Mathlib.SetTheory.Ordinal.Basic Mathlib.SetTheory.Ordinal.Enum Mathlib.SetTheory.Ordinal.Exponential Mathlib.SetTheory.Ordinal.Family Mathlib.SetTheory.Ordinal.FixedPointApproximants Mathlib.SetTheory.Ordinal.FixedPoint Mathlib.SetTheory.Ordinal.NaturalOps Mathlib.SetTheory.Ordinal.Notation Mathlib.SetTheory.Ordinal.Principal Mathlib.SetTheory.Ordinal.Rank Mathlib.SetTheory.Ordinal.Topology Mathlib.SetTheory.Ordinal.Veblen Mathlib.SetTheory.Surreal.Basic Mathlib.SetTheory.ZFC.Cardinal Mathlib.SetTheory.ZFC.Rank Mathlib.SetTheory.ZFC.VonNeumann Mathlib.Tactic.Module Mathlib.Topology.Algebra.ConstMulAction Mathlib.Topology.Algebra.Group.AddTorsor Mathlib.Topology.Algebra.GroupWithZero Mathlib.Topology.Algebra.InfiniteSum.Basic Mathlib.Topology.Algebra.InfiniteSum.Defs Mathlib.Topology.Algebra.Monoid.AddChar Mathlib.Topology.Algebra.Monoid Mathlib.Topology.Algebra.MulAction Mathlib.Topology.Algebra.Order.Module Mathlib.Topology.Algebra.Order.Support Mathlib.Topology.Algebra.ProperConstSMul Mathlib.Topology.Algebra.Star Mathlib.Topology.Algebra.Support Mathlib.Topology.Algebra.WithZeroTopology Mathlib.Topology.ApproximateUnit Mathlib.Topology.Category.CompHausLike.EffectiveEpi Mathlib.Topology.Germ Mathlib.Topology.Instances.ENat Mathlib.Topology.KrullDimension Mathlib.Topology.LocallyConstant.Algebra Mathlib.Topology.Order.Compact Mathlib.Topology.Order.Rolle Mathlib.Topology.Sheaves.Alexandrov Mathlib.Topology.Sheaves.Forget Mathlib.Topology.Sheaves.Functors Mathlib.Topology.Sheaves.Limits Mathlib.Topology.Sheaves.LocalPredicate Mathlib.Topology.Sheaves.LocallySurjective Mathlib.Topology.Sheaves.PUnit Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections Mathlib.Topology.Sheaves.SheafCondition.Sites Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing Mathlib.Topology.Sheaves.SheafOfFunctions Mathlib.Topology.Sheaves.Sheaf Mathlib.Topology.Sheaves.Sheafify Mathlib.Topology.Sheaves.Skyscraper Mathlib.Topology.Sheaves.Stalks Mathlib.Topology.UniformSpace.HeineCantor	2
16 files Mathlib.Algebra.Order.BigOperators.Ring.List Mathlib.Algebra.Order.BigOperators.Ring.Multiset Mathlib.Algebra.Order.Ring.Basic Mathlib.Algebra.Order.Ring.Canonical Mathlib.Algebra.Order.Ring.WithTop Mathlib.Algebra.Order.WithTop.Untop0 Mathlib.Algebra.Ring.Parity Mathlib.Data.Bool.Count Mathlib.Data.Nat.Bitwise Mathlib.Data.Nat.Choose.Dvd Mathlib.Data.Nat.Dist Mathlib.Data.Nat.EvenOddRec Mathlib.Data.Nat.Prime.Basic Mathlib.Data.Nat.Prime.Factorial Mathlib.Data.Nat.Prime.Pow Mathlib.Data.Set.Semiring	3

---

Declarations diff

+ apply_ite_left
+ fib_neg
+ gcd_fib
+ neg_one_zpow_eq_ite
- fib_gcd

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[themathqueen]

I think there's something wrong with the import bot (#32107 (comment)), it keeps saying there's no import change, but there is a change.

[j-loreaux]

I think there's something wrong with the import bot (#32107 (comment)), it keeps saying there's no import change, but there is a change.

This is a consequence of the new module system. The bot isn't smart enough to figure it out yet.

[ocfnash]

Let's wait for #32133 to land and then merge master in here to see about the import change.

[adomani]

I just re-ran the PR summary script: I am not sure what it is supposed to do, but hopefully will pick up the new script on master that should be aware of public imports.

EDIT: it picked up the new script, but the script probably needs some fixing up.

[themathqueen]

I just re-ran the PR summary script: I am not sure what it is supposed to do, but hopefully will pick up the new script on master that should be aware of public imports.

EDIT: it picked up the new script, but the script probably needs some fixing up.

Yeah, but at least it's actually working now! 🎉

[adomani]

Oh yes, it's definitely an improvement! It just needs a final touch-up!

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - chore: fix dependency counting script #32133
  By Dependent Issues (🤖). Happy coding!

[ocfnash]

Thanks!

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style
• Post-Build Step