feat: add telescoping sum theorems to BigOperators.Intervals by jessealama · Pull Request #29643 · leanprover-community/mathlib4

jessealama · 2025-09-14T14:46:11Z

Summary

This PR adds theorems for alternating telescoping sums that will be used in the forthcoming proof of Euler's polyhedron formula.

Theorems Added

sum_negOnePow_smul_add_consecutive_succ: Alternating sum of consecutive pairs (inclusive version, 0 to n)
sum_negOnePow_smul_add_consecutive: Alternating sum of consecutive pairs (standard version, 0 to n-1)

Details

These theorems show that alternating sums of consecutive pairs telescope to boundary terms:

∑ k ∈ Finset.range n, (k : ℤ).negOnePow • (a k + a (k + 1)) = a 0 - (n : ℤ).negOnePow • a n

The theorems are generalized to work with any Module over a Ring, making them broadly applicable beyond just the Euler polyhedron formula use case.

Context

This is the first of several PRs to break up #29639 into smaller, more reviewable pieces as suggested in the review comments.

github-actions · 2025-09-14T14:47:26Z

PR summary 82ba83d8bc

Import changes exceeding 2%

%	File
+52.10%	`Mathlib.Algebra.BigOperators.Ring.Finset`

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Algebra.BigOperators.Ring.Finset	618	940	+322 (+52.10%)

Import changes for all files

Files	Import difference
`Mathlib.LinearAlgebra.TensorProduct.Graded.External` `Mathlib.LinearAlgebra.TensorProduct.Graded.Internal`	1
11 files `Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point` `Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic` `Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree` `Mathlib.AlgebraicGeometry.EllipticCurve.Group` `Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point` `Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point` `Mathlib.FieldTheory.AxGrothendieck` `Mathlib.FieldTheory.IsAlgClosed.Classification` `Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient` `Mathlib.LinearAlgebra.FreeModule.Norm` `Mathlib.ModelTheory.Algebra.Field.IsAlgClosed`	2
33 files `Mathlib.Analysis.SumOverResidueClass` `Mathlib.Combinatorics.SimpleGraph.Acyclic` `Mathlib.Combinatorics.SimpleGraph.Bipartite` `Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite` `Mathlib.Combinatorics.SimpleGraph.ConcreteColorings` `Mathlib.Combinatorics.SimpleGraph.DegreeSum` `Mathlib.Combinatorics.SimpleGraph.Extremal.Turan` `Mathlib.Combinatorics.SimpleGraph.FiveWheelLike` `Mathlib.Combinatorics.SimpleGraph.Girth` `Mathlib.Combinatorics.SimpleGraph.Matching` `Mathlib.Combinatorics.SimpleGraph.Turan` `Mathlib.Combinatorics.SimpleGraph.Tutte` `Mathlib.Combinatorics.SimpleGraph.UniversalVerts` `Mathlib.Data.Nat.Choose.Lucas` `Mathlib.Data.ZMod.Coprime` `Mathlib.Data.ZMod.Factorial` `Mathlib.Data.ZMod.QuotientRing` `Mathlib.Data.ZMod.Units` `Mathlib.GroupTheory.Coxeter.Inversion` `Mathlib.GroupTheory.Coxeter.Length` `Mathlib.LinearAlgebra.FreeModule.Finite.Quotient` `Mathlib.LinearAlgebra.FreeModule.IdealQuotient` `Mathlib.LinearAlgebra.FreeModule.Int` `Mathlib.NumberTheory.DirichletCharacter.Basic` `Mathlib.NumberTheory.FLT.Four` `Mathlib.NumberTheory.LegendreSymbol.ZModChar` `Mathlib.NumberTheory.Padics.ProperSpace` `Mathlib.NumberTheory.Padics.RingHoms` `Mathlib.NumberTheory.Pell` `Mathlib.NumberTheory.PythagoreanTriples` `Mathlib.RingTheory.WittVector.WittPolynomial` `Mathlib.RingTheory.ZMod` `Mathlib.Tactic.ReduceModChar`	3
89 files `Mathlib.AlgebraicGeometry.AffineScheme` `Mathlib.AlgebraicGeometry.Cover.Over` `Mathlib.AlgebraicGeometry.Cover.Sigma` `Mathlib.AlgebraicGeometry.FunctionField` `Mathlib.AlgebraicGeometry.GluingOneHypercover` `Mathlib.AlgebraicGeometry.IdealSheaf.Basic` `Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme` `Mathlib.AlgebraicGeometry.IdealSheaf` `Mathlib.AlgebraicGeometry.Limits` `Mathlib.AlgebraicGeometry.Morphisms.AffineAnd` `Mathlib.AlgebraicGeometry.Morphisms.Affine` `Mathlib.AlgebraicGeometry.Morphisms.Basic` `Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion` `Mathlib.AlgebraicGeometry.Morphisms.Constructors` `Mathlib.AlgebraicGeometry.Morphisms.Descent` `Mathlib.AlgebraicGeometry.Morphisms.FiniteType` `Mathlib.AlgebraicGeometry.Morphisms.IsIso` `Mathlib.AlgebraicGeometry.Morphisms.LocalClosure` `Mathlib.AlgebraicGeometry.Morphisms.LocalIso` `Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion` `Mathlib.AlgebraicGeometry.Morphisms.Preimmersion` `Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact` `Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated` `Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties` `Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks` `Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap` `Mathlib.AlgebraicGeometry.Noetherian` `Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic` `Mathlib.AlgebraicGeometry.Properties` `Mathlib.AlgebraicGeometry.Pullbacks` `Mathlib.AlgebraicGeometry.ResidueField` `Mathlib.AlgebraicGeometry.Sites.BigZariski` `Mathlib.AlgebraicGeometry.Sites.MorphismProperty` `Mathlib.AlgebraicGeometry.Sites.Representability` `Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski` `Mathlib.AlgebraicGeometry.Sites.Small` `Mathlib.AlgebraicGeometry.SpreadingOut` `Mathlib.AlgebraicGeometry.Stalk` `Mathlib.Analysis.Analytic.Polynomial` `Mathlib.Analysis.Calculus.Implicit` `Mathlib.Analysis.Complex.OperatorNorm` `Mathlib.Analysis.Convex.Cone.Dual` `Mathlib.Analysis.Convex.KreinMilman` `Mathlib.Analysis.LocallyConvex.WeakSpace` `Mathlib.Analysis.Normed.Module.Complemented` `Mathlib.Analysis.NormedSpace.HahnBanach.Separation` `Mathlib.CategoryTheory.Preadditive.Schur` `Mathlib.Combinatorics.Derangements.Exponential` `Mathlib.FieldTheory.AlgebraicClosure` `Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure` `Mathlib.FieldTheory.IsAlgClosed.Basic` `Mathlib.FieldTheory.IsAlgClosed.Spectrum` `Mathlib.FieldTheory.PerfectClosure` `Mathlib.FieldTheory.Perfect` `Mathlib.FieldTheory.SeparableDegree` `Mathlib.LinearAlgebra.AffineSpace.Matrix` `Mathlib.LinearAlgebra.Complex.Determinant` `Mathlib.LinearAlgebra.Complex.Orientation` `Mathlib.LinearAlgebra.Eigenspace.Pi` `Mathlib.LinearAlgebra.Eigenspace.Triangularizable` `Mathlib.LinearAlgebra.Eigenspace.Zero` `Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs` `Mathlib.LinearAlgebra.Matrix.Gershgorin` `Mathlib.MeasureTheory.Constructions.BorelSpace.ContinuousLinearMap` `Mathlib.ModelTheory.Algebra.Ring.Definability` `Mathlib.NumberTheory.KummerDedekind` `Mathlib.RepresentationTheory.Character` `Mathlib.RepresentationTheory.FDRep` `Mathlib.RepresentationTheory.GroupCohomology.Functoriality` `Mathlib.RepresentationTheory.GroupCohomology.Hilbert90` `Mathlib.RepresentationTheory.GroupCohomology.LowDegree` `Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality` `Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90` `Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence` `Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree` `Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality` `Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence` `Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree` `Mathlib.RepresentationTheory.Invariants` `Mathlib.RepresentationTheory.Tannaka` `Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure` `Mathlib.RingTheory.DedekindDomain.Factorization` `Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas` `Mathlib.RingTheory.Nullstellensatz` `Mathlib.RingTheory.SimpleModule.IsAlgClosed` `Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity` `Mathlib.RingTheory.Spectrum.Prime.Polynomial` `Mathlib.Topology.Algebra.Module.Determinant` `Mathlib.Topology.Algebra.Module.FiniteDimension`	5
248 files `Mathlib.Algebra.BrauerGroup.Defs` `Mathlib.Algebra.DirectSum.LinearMap` `Mathlib.Algebra.GCDMonoid.IntegrallyClosed` `Mathlib.Algebra.Module.LinearMap.Polynomial` `Mathlib.Algebra.Polynomial.Bivariate` `Mathlib.AlgebraicGeometry.Cover.MorphismProperty` `Mathlib.AlgebraicGeometry.Cover.Open` `Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic` `Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula` `Mathlib.AlgebraicGeometry.EllipticCurve.Affine` `Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic` `Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula` `Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic` `Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula` `Mathlib.AlgebraicGeometry.GammaSpecAdjunction` `Mathlib.AlgebraicGeometry.Gluing` `Mathlib.AlgebraicGeometry.Modules.Presheaf` `Mathlib.AlgebraicGeometry.Modules.Sheaf` `Mathlib.AlgebraicGeometry.Modules.Tilde` `Mathlib.AlgebraicGeometry.OpenImmersion` `Mathlib.AlgebraicGeometry.Over` `Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme` `Mathlib.AlgebraicGeometry.Restrict` `Mathlib.AlgebraicGeometry.Scheme` `Mathlib.AlgebraicGeometry.Spec` `Mathlib.AlgebraicGeometry.StructureSheaf` `Mathlib.Analysis.CStarAlgebra.Classes` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Pi` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unitary` `Mathlib.Analysis.CStarAlgebra.ContinuousMap` `Mathlib.Analysis.CStarAlgebra.Exponential` `Mathlib.Analysis.CStarAlgebra.Unitization` `Mathlib.Analysis.Calculus.Conformal.InnerProduct` `Mathlib.Analysis.Calculus.ContDiff.RCLike` `Mathlib.Analysis.Calculus.Deriv.MeanValue` `Mathlib.Analysis.Calculus.DerivativeTest` `Mathlib.Analysis.Calculus.FDeriv.Extend` `Mathlib.Analysis.Calculus.FDeriv.Symmetric` `Mathlib.Analysis.Calculus.InverseFunctionTheorem.ContDiff` `Mathlib.Analysis.Calculus.LHopital` `Mathlib.Analysis.Calculus.LogDeriv` `Mathlib.Analysis.Calculus.MeanValue` `Mathlib.Analysis.Calculus.SmoothSeries` `Mathlib.Analysis.Calculus.Taylor` `Mathlib.Analysis.Calculus.UniformLimitsDeriv` `Mathlib.Analysis.Calculus.VectorField` `Mathlib.Analysis.Complex.AbelLimit` `Mathlib.Analysis.Complex.Asymptotics` `Mathlib.Analysis.Complex.Basic` `Mathlib.Analysis.Complex.Convex` `Mathlib.Analysis.Complex.ExponentialBounds` `Mathlib.Analysis.Complex.HalfPlane` `Mathlib.Analysis.Complex.IntegerCompl` `Mathlib.Analysis.Complex.IsIntegral` `Mathlib.Analysis.Complex.ReImTopology` `Mathlib.Analysis.Complex.RealDeriv` `Mathlib.Analysis.Complex.UpperHalfPlane.Basic` `Mathlib.Analysis.Complex.ValueDistribution.CountingFunction` `Mathlib.Analysis.ConstantSpeed` `Mathlib.Analysis.Convex.Deriv` `Mathlib.Analysis.Convex.GaugeRescale` `Mathlib.Analysis.Convex.Gauge` `Mathlib.Analysis.Convex.Strong` `Mathlib.Analysis.InnerProductSpace.Affine` `Mathlib.Analysis.InnerProductSpace.Basic` `Mathlib.Analysis.InnerProductSpace.Completion` `Mathlib.Analysis.InnerProductSpace.ConformalLinearMap` `Mathlib.Analysis.InnerProductSpace.Continuous` `Mathlib.Analysis.InnerProductSpace.Convex` `Mathlib.Analysis.InnerProductSpace.Defs` `Mathlib.Analysis.InnerProductSpace.LinearMap` `Mathlib.Analysis.InnerProductSpace.OfNorm` `Mathlib.Analysis.InnerProductSpace.Orthogonal` `Mathlib.Analysis.InnerProductSpace.Orthonormal` `Mathlib.Analysis.InnerProductSpace.Projection.Minimal` `Mathlib.Analysis.InnerProductSpace.Subspace` `Mathlib.Analysis.InnerProductSpace.Symmetric` `Mathlib.Analysis.LocallyConvex.AbsConvexOpen` `Mathlib.Analysis.LocallyConvex.ContinuousOfBounded` `Mathlib.Analysis.Meromorphic.FactorizedRational` `Mathlib.Analysis.Normed.Algebra.Exponential` `Mathlib.Analysis.Normed.Group.Tannery` `Mathlib.Analysis.Normed.Module.RCLike.Basic` `Mathlib.Analysis.NormedSpace.Extend` `Mathlib.Analysis.NormedSpace.Normalize` `Mathlib.Analysis.NormedSpace.RCLike` `Mathlib.Analysis.ODE.Gronwall` `Mathlib.Analysis.RCLike.Basic` `Mathlib.Analysis.RCLike.BoundedContinuous` `Mathlib.Analysis.RCLike.TangentCone` `Mathlib.Analysis.SpecialFunctions.Bernstein` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic` `Mathlib.Analysis.SpecialFunctions.ExpDeriv` `Mathlib.Analysis.SpecialFunctions.Exp` `Mathlib.Analysis.SpecialFunctions.Exponential` `Mathlib.Analysis.SpecialFunctions.Log.Basic` `Mathlib.Analysis.SpecialFunctions.Log.Deriv` `Mathlib.Analysis.SpecialFunctions.Log.PosLog` `Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq` `Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric` `Mathlib.Analysis.SpecialFunctions.Pochhammer` `Mathlib.Analysis.SpecialFunctions.PolynomialExp` `Mathlib.Analysis.SpecialFunctions.SmoothTransition` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Series` `Mathlib.Analysis.SpecificLimits.RCLike` `Mathlib.Combinatorics.Configuration` `Mathlib.Data.Complex.ExponentialBounds` `Mathlib.Deprecated.AnalyticManifold` `Mathlib.Dynamics.BirkhoffSum.NormedSpace` `Mathlib.FieldTheory.Extension` `Mathlib.FieldTheory.Fixed` `Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra` `Mathlib.FieldTheory.IntermediateField.Adjoin.Basic` `Mathlib.FieldTheory.IntermediateField.Algebraic` `Mathlib.FieldTheory.KummerPolynomial` `Mathlib.FieldTheory.Minpoly.ConjRootClass` `Mathlib.FieldTheory.Minpoly.Field` `Mathlib.FieldTheory.Minpoly.IsConjRoot` `Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed` `Mathlib.FieldTheory.Normal.Basic` `Mathlib.FieldTheory.Normal.Closure` `Mathlib.FieldTheory.Normal.Defs` `Mathlib.FieldTheory.RatFunc.Basic` `Mathlib.FieldTheory.Relrank` `Mathlib.FieldTheory.Separable` `Mathlib.FieldTheory.SplittingField.Construction` `Mathlib.FieldTheory.SplittingField.IsSplittingField` `Mathlib.Geometry.Euclidean.Basic` `Mathlib.Geometry.Euclidean.Inversion.Basic` `Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane` `Mathlib.Geometry.Euclidean.PerpBisector` `Mathlib.Geometry.Manifold.AnalyticManifold` `Mathlib.Geometry.Manifold.IsManifold.Basic` `Mathlib.LinearAlgebra.AnnihilatingPolynomial` `Mathlib.LinearAlgebra.Charpoly.BaseChange` `Mathlib.LinearAlgebra.Charpoly.Basic` `Mathlib.LinearAlgebra.Charpoly.ToMatrix` `Mathlib.LinearAlgebra.CrossProduct` `Mathlib.LinearAlgebra.Determinant` `Mathlib.LinearAlgebra.Eigenspace.Minpoly` `Mathlib.LinearAlgebra.FreeModule.Determinant` `Mathlib.LinearAlgebra.Lagrange` `Mathlib.LinearAlgebra.Matrix.AbsoluteValue` `Mathlib.LinearAlgebra.Matrix.Adjugate` `Mathlib.LinearAlgebra.Matrix.BaseChange` `Mathlib.LinearAlgebra.Matrix.Basis` `Mathlib.LinearAlgebra.Matrix.Block` `Mathlib.LinearAlgebra.Matrix.Charpoly.Basic` `Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff` `Mathlib.LinearAlgebra.Matrix.Charpoly.Disc` `Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap` `Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly` `Mathlib.LinearAlgebra.Matrix.Charpoly.Univ` `Mathlib.LinearAlgebra.Matrix.Determinant.Basic` `Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular` `Mathlib.LinearAlgebra.Matrix.IsDiag` `Mathlib.LinearAlgebra.Matrix.Kronecker` `Mathlib.LinearAlgebra.Matrix.MvPolynomial` `Mathlib.LinearAlgebra.Matrix.Nondegenerate` `Mathlib.LinearAlgebra.Matrix.NonsingularInverse` `Mathlib.LinearAlgebra.Matrix.Polynomial` `Mathlib.LinearAlgebra.Matrix.Rank` `Mathlib.LinearAlgebra.Matrix.Reindex` `Mathlib.LinearAlgebra.Matrix.Transvection` `Mathlib.LinearAlgebra.Matrix.Vec` `Mathlib.LinearAlgebra.Matrix.ZPow` `Mathlib.LinearAlgebra.Orientation` `Mathlib.LinearAlgebra.PID` `Mathlib.LinearAlgebra.PerfectPairing.Restrict` `Mathlib.LinearAlgebra.Projectivization.Constructions` `Mathlib.LinearAlgebra.SymplecticGroup` `Mathlib.LinearAlgebra.TensorProduct.Matrix` `Mathlib.LinearAlgebra.Trace` `Mathlib.LinearAlgebra.UnitaryGroup` `Mathlib.LinearAlgebra.Vandermonde` `Mathlib.MeasureTheory.Constructions.BorelSpace.Complex` `Mathlib.MeasureTheory.Function.SpecialFunctions.Inner` `Mathlib.MeasureTheory.Measure.Complex` `Mathlib.NumberTheory.Transcendental.Liouville.Basic` `Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber` `Mathlib.NumberTheory.VonMangoldt` `Mathlib.RingTheory.Adjoin.Field` `Mathlib.RingTheory.Adjoin.PowerBasis` `Mathlib.RingTheory.AdjoinRoot` `Mathlib.RingTheory.Algebraic.Integral` `Mathlib.RingTheory.AlgebraicIndependent.Adjoin` `Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality` `Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis` `Mathlib.RingTheory.ClassGroup` `Mathlib.RingTheory.Conductor` `Mathlib.RingTheory.DedekindDomain.Basic` `Mathlib.RingTheory.DedekindDomain.Ideal.Basic` `Mathlib.RingTheory.Derivation.MapCoeffs` `Mathlib.RingTheory.Ideal.GoingUp` `Mathlib.RingTheory.Ideal.Height` `Mathlib.RingTheory.IntegralClosure.Algebra.Basic` `Mathlib.RingTheory.IntegralClosure.IntegrallyClosed` `Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic` `Mathlib.RingTheory.IsAdjoinRoot` `Mathlib.RingTheory.Jacobson.Ring` `Mathlib.RingTheory.KrullDimension.Module` `Mathlib.RingTheory.KrullDimension.PID` `Mathlib.RingTheory.KrullDimension.Polynomial` `Mathlib.RingTheory.KrullDimension.Zero` `Mathlib.RingTheory.LocalProperties.IntegrallyClosed` `Mathlib.RingTheory.LocalRing.ResidueField.Instances` `Mathlib.RingTheory.Localization.Away.AdjoinRoot` `Mathlib.RingTheory.Localization.Integral` `Mathlib.RingTheory.Localization.Pi` `Mathlib.RingTheory.MatrixAlgebra` `Mathlib.RingTheory.MatrixPolynomialAlgebra` `Mathlib.RingTheory.NoetherNormalization` `Mathlib.RingTheory.Norm.Defs` `Mathlib.RingTheory.Norm.Transitivity` `Mathlib.RingTheory.Polynomial.DegreeLT` `Mathlib.RingTheory.Polynomial.GaussLemma` `Mathlib.RingTheory.Polynomial.Hermite.Gaussian` `Mathlib.RingTheory.Polynomial.RationalRoot` `Mathlib.RingTheory.Polynomial.Resultant.Basic` `Mathlib.RingTheory.Polynomial.SeparableDegree` `Mathlib.RingTheory.PowerBasis` `Mathlib.RingTheory.RingHom.FinitePresentation` `Mathlib.RingTheory.RingHom.Integral` `Mathlib.RingTheory.Spectrum.Maximal.Topology` `Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet` `Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC` `Mathlib.RingTheory.Spectrum.Prime.Jacobson` `Mathlib.RingTheory.Spectrum.Prime.Module` `Mathlib.RingTheory.Spectrum.Prime.Noetherian` `Mathlib.RingTheory.Spectrum.Prime.TensorProduct` `Mathlib.RingTheory.Spectrum.Prime.Topology` `Mathlib.RingTheory.Valuation.AlgebraInstances` `Mathlib.RingTheory.Valuation.Archimedean` `Mathlib.RingTheory.Valuation.Integral` `Mathlib.RingTheory.Valuation.IntegrallyClosed` `Mathlib.RingTheory.Valuation.LocalSubring` `Mathlib.RingTheory.Valuation.Minpoly` `Mathlib.Tactic.FunProp.ContDiff` `Mathlib.Tactic.FunProp.Differentiable` `Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn` `Mathlib.Topology.Algebra.Valued.WithZeroMulInt` `Mathlib.Topology.ContinuousMap.ContinuousSqrt` `Mathlib.Topology.ContinuousMap.Ideals` `Mathlib.Topology.ContinuousMap.StoneWeierstrass` `Mathlib.Topology.ContinuousMap.Weierstrass` `Mathlib.Topology.Instances.Complex` `Mathlib.Topology.VectorBundle.Riemannian`	6
4 files `Mathlib.Algebra.CharP.Quotient` `Mathlib.Analysis.Normed.Ring.Finite` `Mathlib.LinearAlgebra.Alternating.Uncurry.Fin` `Mathlib.NumberTheory.MulChar.Basic`	7
`Mathlib.Algebra.CharP.CharAndCard`	8
`Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer` `Mathlib.GroupTheory.SpecificGroups.Alternating`	11
`Mathlib.NumberTheory.Padics.Hensel`	12
3 files `Mathlib.Algebra.CharP.Two` `Mathlib.NumberTheory.Padics.PadicIntegers` `Mathlib.SetTheory.Nimber.Field`	13
6 files `Mathlib.GroupTheory.FixedPointFree` `Mathlib.GroupTheory.Perm.Centralizer` `Mathlib.GroupTheory.Perm.Cycle.Concrete` `Mathlib.GroupTheory.Perm.Cycle.PossibleTypes` `Mathlib.GroupTheory.Perm.Cycle.Type` `Mathlib.GroupTheory.Perm.Fin`	14
`Mathlib.GroupTheory.Exponent` `Mathlib.GroupTheory.GroupAction.Period`	15
`Mathlib.NumberTheory.EulerProduct.Basic` `Mathlib.NumberTheory.TsumDivsorsAntidiagonal`	16
`Mathlib.RepresentationTheory.FiniteIndex`	17
4 files `Mathlib.Analysis.LocallyConvex.WeakDual` `Mathlib.LinearAlgebra.Complex.FiniteDimensional` `Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic` `Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits`	18
17 files `Mathlib.Analysis.Convex.AmpleSet` `Mathlib.Analysis.Convex.Side` `Mathlib.Analysis.Convex.StrictConvexBetween` `Mathlib.Analysis.NormedSpace.Connected` `Mathlib.RepresentationTheory.Coinduced` `Mathlib.RepresentationTheory.Coinvariants` `Mathlib.RepresentationTheory.GroupCohomology.Basic` `Mathlib.RepresentationTheory.GroupCohomology.Resolution` `Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic` `Mathlib.RepresentationTheory.Homological.GroupCohomology.Shapiro` `Mathlib.RepresentationTheory.Homological.GroupHomology.Basic` `Mathlib.RepresentationTheory.Homological.GroupHomology.Shapiro` `Mathlib.RepresentationTheory.Homological.Resolution` `Mathlib.RepresentationTheory.Induced` `Mathlib.RepresentationTheory.Rep` `Mathlib.Topology.Category.Profinite.Nobeling.Induction` `Mathlib.Topology.Category.Profinite.Nobeling`	19
`Mathlib.RingTheory.LocalRing.Quotient`	20
15 files `Mathlib.Analysis.Analytic.IteratedFDeriv` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital` `Mathlib.Analysis.Calculus.AddTorsor.AffineMap` `Mathlib.Analysis.Calculus.ContDiff.Basic` `Mathlib.Analysis.Calculus.ContDiff.Bounds` `Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno` `Mathlib.Analysis.Calculus.ContDiff.Operations` `Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno` `Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas` `Mathlib.Analysis.Calculus.LocalExtr.Polynomial` `Mathlib.Analysis.SpecialFunctions.Sqrt` `Mathlib.LinearAlgebra.Projectivization.Cardinality` `Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic`	21
132 files `Mathlib.Analysis.Analytic.Basic` `Mathlib.Analysis.Analytic.CPolynomialDef` `Mathlib.Analysis.Analytic.CPolynomial` `Mathlib.Analysis.Analytic.ChangeOrigin` `Mathlib.Analysis.Analytic.Composition` `Mathlib.Analysis.Analytic.Constructions` `Mathlib.Analysis.Analytic.ConvergenceRadius` `Mathlib.Analysis.Analytic.Inverse` `Mathlib.Analysis.Analytic.IsolatedZeros` `Mathlib.Analysis.Analytic.Linear` `Mathlib.Analysis.Analytic.OfScalars` `Mathlib.Analysis.Analytic.Order` `Mathlib.Analysis.Analytic.Uniqueness` `Mathlib.Analysis.Analytic.Within` `Mathlib.Analysis.Calculus.Conformal.NormedSpace` `Mathlib.Analysis.Calculus.ContDiff.CPolynomial` `Mathlib.Analysis.Calculus.ContDiff.Defs` `Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries` `Mathlib.Analysis.Calculus.ContDiff.RestrictScalars` `Mathlib.Analysis.Calculus.DSlope` `Mathlib.Analysis.Calculus.Darboux` `Mathlib.Analysis.Calculus.Deriv.Add` `Mathlib.Analysis.Calculus.Deriv.AffineMap` `Mathlib.Analysis.Calculus.Deriv.CompMul` `Mathlib.Analysis.Calculus.Deriv.Inv` `Mathlib.Analysis.Calculus.Deriv.Inverse` `Mathlib.Analysis.Calculus.Deriv.Linear` `Mathlib.Analysis.Calculus.Deriv.Mul` `Mathlib.Analysis.Calculus.Deriv.Pi` `Mathlib.Analysis.Calculus.Deriv.Polynomial` `Mathlib.Analysis.Calculus.Deriv.Pow` `Mathlib.Analysis.Calculus.Deriv.Prod` `Mathlib.Analysis.Calculus.Deriv.Shift` `Mathlib.Analysis.Calculus.Deriv.Slope` `Mathlib.Analysis.Calculus.Deriv.Star` `Mathlib.Analysis.Calculus.Deriv.ZPow` `Mathlib.Analysis.Calculus.DiffContOnCl` `Mathlib.Analysis.Calculus.FDeriv.Add` `Mathlib.Analysis.Calculus.FDeriv.Analytic` `Mathlib.Analysis.Calculus.FDeriv.Bilinear` `Mathlib.Analysis.Calculus.FDeriv.Equiv` `Mathlib.Analysis.Calculus.FDeriv.Linear` `Mathlib.Analysis.Calculus.FDeriv.Mul` `Mathlib.Analysis.Calculus.FDeriv.Pi` `Mathlib.Analysis.Calculus.FDeriv.Pow` `Mathlib.Analysis.Calculus.FDeriv.Prod` `Mathlib.Analysis.Calculus.FDeriv.Star` `Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn` `Mathlib.Analysis.Calculus.InverseFunctionTheorem.Deriv` `Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv` `Mathlib.Analysis.Calculus.IteratedDeriv.Defs` `Mathlib.Analysis.Calculus.IteratedDeriv.WithinZpow` `Mathlib.Analysis.Calculus.LagrangeMultipliers` `Mathlib.Analysis.Calculus.LineDeriv.Basic` `Mathlib.Analysis.Calculus.LocalExtr.Basic` `Mathlib.Analysis.Calculus.LocalExtr.LineDeriv` `Mathlib.Analysis.Calculus.LocalExtr.Rolle` `Mathlib.Analysis.Convex.PartitionOfUnity` `Mathlib.Analysis.Meromorphic.Basic` `Mathlib.Analysis.Meromorphic.Divisor` `Mathlib.Analysis.Meromorphic.IsolatedZeros` `Mathlib.Analysis.Meromorphic.NormalForm` `Mathlib.Analysis.Meromorphic.Order` `Mathlib.Analysis.Meromorphic.TrailingCoefficient` `Mathlib.Analysis.Normed.Group.Quotient` `Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels` `Mathlib.Analysis.Normed.Operator.Banach` `Mathlib.Analysis.Normed.Operator.BoundedLinearMaps` `Mathlib.Condensed.AB` `Mathlib.Condensed.Discrete.Basic` `Mathlib.Condensed.Discrete.Characterization` `Mathlib.Condensed.Discrete.Colimit` `Mathlib.Condensed.Discrete.LocallyConstant` `Mathlib.Condensed.Discrete.Module` `Mathlib.Condensed.Epi` `Mathlib.Condensed.Equivalence` `Mathlib.Condensed.Explicit` `Mathlib.Condensed.Functors` `Mathlib.Condensed.Light.AB` `Mathlib.Condensed.Light.Basic` `Mathlib.Condensed.Light.CartesianClosed` `Mathlib.Condensed.Light.Epi` `Mathlib.Condensed.Light.Explicit` `Mathlib.Condensed.Light.Functors` `Mathlib.Condensed.Light.Limits` `Mathlib.Condensed.Light.Module` `Mathlib.Condensed.Light.TopCatAdjunction` `Mathlib.Condensed.Light.TopComparison` `Mathlib.Condensed.Limits` `Mathlib.Condensed.Module` `Mathlib.Condensed.Solid` `Mathlib.Data.Real.GoldenRatio` `Mathlib.Geometry.Manifold.ConformalGroupoid` `Mathlib.RingTheory.Ideal.Quotient.Index` `Mathlib.RingTheory.PowerSeries.Evaluation` `Mathlib.RingTheory.PowerSeries.Substitution` `Mathlib.Topology.Algebra.IsOpenUnits` `Mathlib.Topology.Algebra.Module.Cardinality` `Mathlib.Topology.Algebra.Valued.ValuationTopology` `Mathlib.Topology.Algebra.Valued.ValuativeRel` `Mathlib.Topology.Algebra.Valued.ValuedField` `Mathlib.Topology.Category.Compactum` `Mathlib.Topology.Category.LightProfinite.AsLimit` `Mathlib.Topology.Category.LightProfinite.Basic` `Mathlib.Topology.Category.LightProfinite.EffectiveEpi` `Mathlib.Topology.Category.LightProfinite.Extend` `Mathlib.Topology.Category.LightProfinite.Limits` `Mathlib.Topology.Category.LightProfinite.Sequence` `Mathlib.Topology.Category.Profinite.AsLimit` `Mathlib.Topology.Category.Profinite.Basic` `Mathlib.Topology.Category.Profinite.CofilteredLimit` `Mathlib.Topology.Category.Profinite.EffectiveEpi` `Mathlib.Topology.Category.Profinite.Extend` `Mathlib.Topology.Category.Profinite.Limits` `Mathlib.Topology.Category.Profinite.Nobeling.Basic` `Mathlib.Topology.Category.Profinite.Nobeling.Span` `Mathlib.Topology.Category.Profinite.Nobeling.Successor` `Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit` `Mathlib.Topology.Category.Profinite.Product` `Mathlib.Topology.Category.Profinite.Projective` `Mathlib.Topology.Category.Stonean.Adjunctions` `Mathlib.Topology.Category.Stonean.Basic` `Mathlib.Topology.Category.Stonean.EffectiveEpi` `Mathlib.Topology.Category.Stonean.Limits` `Mathlib.Topology.ContinuousMap.Units` `Mathlib.Topology.MetricSpace.PartitionOfUnity` `Mathlib.Topology.Separation.NotNormal` `Mathlib.Topology.Sheaves.CommRingCat` `Mathlib.Topology.TietzeExtension` `Mathlib.Topology.VectorBundle.Basic` `Mathlib.Topology.VectorBundle.Constructions` `Mathlib.Topology.VectorBundle.Hom`	22
93 files `Mathlib.Analysis.Normed.Group.ControlledClosure` `Mathlib.Analysis.Normed.Ring.Units` `Mathlib.Analysis.Real.OfDigits` `Mathlib.Analysis.SpecificLimits.Normed` `Mathlib.Condensed.Basic` `Mathlib.Condensed.CartesianClosed` `Mathlib.Condensed.TopCatAdjunction` `Mathlib.Condensed.TopComparison` `Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber` `Mathlib.Dynamics.Ergodic.Action.Basic` `Mathlib.Dynamics.Ergodic.Conservative` `Mathlib.Dynamics.Ergodic.Ergodic` `Mathlib.Dynamics.Ergodic.MeasurePreserving` `Mathlib.MeasureTheory.Constructions.BorelSpace.Basic` `Mathlib.MeasureTheory.Constructions.BorelSpace.Metric` `Mathlib.MeasureTheory.Constructions.BorelSpace.Order` `Mathlib.MeasureTheory.Constructions.ClosedCompactCylinders` `Mathlib.MeasureTheory.Constructions.Polish.Basic` `Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal` `Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent` `Mathlib.MeasureTheory.Constructions.Projective` `Mathlib.MeasureTheory.Covering.Vitali` `Mathlib.MeasureTheory.Function.AEMeasurableOrder` `Mathlib.MeasureTheory.Function.EssSup` `Mathlib.MeasureTheory.Function.Floor` `Mathlib.MeasureTheory.Function.SimpleFunc` `Mathlib.MeasureTheory.Group.AEStabilizer` `Mathlib.MeasureTheory.Group.Action` `Mathlib.MeasureTheory.Group.Arithmetic` `Mathlib.MeasureTheory.Group.MeasurableEquiv` `Mathlib.MeasureTheory.Group.Pointwise` `Mathlib.MeasureTheory.Integral.Lebesgue.Basic` `Mathlib.MeasureTheory.Integral.Lebesgue.MeasurePreserving` `Mathlib.MeasureTheory.Integral.Lebesgue.Norm` `Mathlib.MeasureTheory.Measure.AEMeasurable` `Mathlib.MeasureTheory.Measure.Content` `Mathlib.MeasureTheory.Measure.ContinuousPreimage` `Mathlib.MeasureTheory.Measure.Count` `Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion` `Mathlib.MeasureTheory.Measure.Decomposition.Hahn` `Mathlib.MeasureTheory.Measure.Dirac` `Mathlib.MeasureTheory.Measure.MutuallySingular` `Mathlib.MeasureTheory.Measure.OpenPos` `Mathlib.MeasureTheory.Measure.Real` `Mathlib.MeasureTheory.Measure.Regular` `Mathlib.MeasureTheory.Measure.RegularityCompacts` `Mathlib.MeasureTheory.Measure.Restrict` `Mathlib.MeasureTheory.Measure.Stieltjes` `Mathlib.MeasureTheory.Measure.Sub` `Mathlib.MeasureTheory.Measure.Support` `Mathlib.MeasureTheory.Measure.Tight` `Mathlib.MeasureTheory.Measure.Trim` `Mathlib.MeasureTheory.Measure.Typeclasses.Finite` `Mathlib.MeasureTheory.Measure.Typeclasses.NoAtoms` `Mathlib.MeasureTheory.Measure.Typeclasses.Probability` `Mathlib.MeasureTheory.Measure.Typeclasses.SFinite` `Mathlib.MeasureTheory.Measure.Typeclasses` `Mathlib.MeasureTheory.Measure.WithDensityFinite` `Mathlib.MeasureTheory.Order.Group.Lattice` `Mathlib.MeasureTheory.Order.Lattice` `Mathlib.MeasureTheory.OuterMeasure.OfAddContent` `Mathlib.MeasureTheory.Topology` `Mathlib.MeasureTheory.VectorMeasure.Basic` `Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn` `Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub` `Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan` `Mathlib.Probability.ConditionalProbability` `Mathlib.Probability.ProbabilityMassFunction.Basic` `Mathlib.Probability.ProbabilityMassFunction.Binomial` `Mathlib.Probability.ProbabilityMassFunction.Constructions` `Mathlib.Probability.ProbabilityMassFunction.Monad` `Mathlib.Probability.UniformOn` `Mathlib.RingTheory.PowerSeries.PiTopology` `Mathlib.Topology.Algebra.Module.PerfectSpace` `Mathlib.Topology.Algebra.Module.Simple` `Mathlib.Topology.Algebra.ProperAction.ProperlyDiscontinuous` `Mathlib.Topology.Baire.BaireMeasurable` `Mathlib.Topology.Category.CompHaus.Basic` `Mathlib.Topology.Category.CompHaus.EffectiveEpi` `Mathlib.Topology.Category.CompHaus.Frm` `Mathlib.Topology.Category.CompHaus.Limits` `Mathlib.Topology.Category.CompHaus.Projective` `Mathlib.Topology.Category.CompactlyGenerated` `Mathlib.Topology.Category.Locale` `Mathlib.Topology.Compactness.CompactlyGeneratedSpace` `Mathlib.Topology.Maps.Proper.CompactlyGenerated` `Mathlib.Topology.Metrizable.Urysohn` `Mathlib.Topology.Order.Category.FrameAdjunction` `Mathlib.Topology.PartitionOfUnity` `Mathlib.Topology.Separation.CompletelyRegular` `Mathlib.Topology.Separation.Lemmas` `Mathlib.Topology.UrysohnsBounded` `Mathlib.Topology.UrysohnsLemma`	23
39 files `Mathlib.Analysis.Calculus.Deriv.Basic` `Mathlib.Analysis.Calculus.Deriv.Comp` `Mathlib.Analysis.Calculus.Deriv.Support` `Mathlib.Analysis.Calculus.FDeriv.Basic` `Mathlib.Analysis.Calculus.FDeriv.Comp` `Mathlib.Analysis.Calculus.FDeriv.Congr` `Mathlib.Analysis.Calculus.FDeriv.Const` `Mathlib.Analysis.Calculus.FDeriv.RestrictScalars` `Mathlib.Analysis.Calculus.TangentCone` `Mathlib.Analysis.Convex.Body` `Mathlib.Analysis.Convex.StrictConvexSpace` `Mathlib.Analysis.Convex.Uniform` `Mathlib.Analysis.Normed.Group.ZeroAtInfty` `Mathlib.Analysis.Normed.Module.Ball.Homeomorph` `Mathlib.Analysis.Normed.Module.Ball.Pointwise` `Mathlib.Analysis.Normed.Module.Convex` `Mathlib.Analysis.Normed.Operator.BanachSteinhaus` `Mathlib.Analysis.NormedSpace.HomeomorphBall` `Mathlib.Analysis.NormedSpace.Pointwise` `Mathlib.Analysis.NormedSpace.RieszLemma` `Mathlib.Dynamics.BirkhoffSum.QuasiMeasurePreserving` `Mathlib.MeasureTheory.Covering.VitaliFamily` `Mathlib.MeasureTheory.Group.Defs` `Mathlib.MeasureTheory.Measure.AbsolutelyContinuous` `Mathlib.MeasureTheory.Measure.Comap` `Mathlib.MeasureTheory.Measure.Map` `Mathlib.MeasureTheory.Measure.MeasureSpace` `Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving` `Mathlib.RingTheory.MvPowerSeries.Evaluation` `Mathlib.RingTheory.MvPowerSeries.Substitution` `Mathlib.Topology.ContinuousMap.Bounded.Star` `Mathlib.Topology.ContinuousMap.Compact` `Mathlib.Topology.ContinuousMap.CompactlySupported` `Mathlib.Topology.ContinuousMap.ContinuousMapZero` `Mathlib.Topology.ContinuousMap.StarOrdered` `Mathlib.Topology.ContinuousMap.ZeroAtInfty` `Mathlib.Topology.MetricSpace.GromovHausdorffRealized` `Mathlib.Topology.MetricSpace.Ultra.ContinuousMaps` `Mathlib.Topology.MetricSpace.UniformConvergence`	24
44 files `Mathlib.Algebra.ArithmeticGeometric` `Mathlib.Analysis.Asymptotics.LinearGrowth` `Mathlib.Analysis.BoxIntegral.Box.SubboxInduction` `Mathlib.Analysis.BoxIntegral.Partition.Filter` `Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction` `Mathlib.Analysis.Complex.Cardinality` `Mathlib.Analysis.Hofer` `Mathlib.Analysis.Normed.Field.ProperSpace` `Mathlib.Analysis.Normed.Group.Completeness` `Mathlib.Analysis.Normed.Group.Pointwise` `Mathlib.Analysis.Normed.Order.UpperLower` `Mathlib.Analysis.Real.Cardinality` `Mathlib.Analysis.Real.Hyperreal` `Mathlib.Analysis.SpecialFunctions.Choose` `Mathlib.Analysis.SpecificLimits.Basic` `Mathlib.Data.Real.Cardinality` `Mathlib.Data.Real.Hyperreal` `Mathlib.Data.Real.Irrational` `Mathlib.FieldTheory.MvRatFunc.Rank` `Mathlib.MeasureTheory.Function.AEMeasurableSequence` `Mathlib.MeasureTheory.Measure.AEDisjoint` `Mathlib.MeasureTheory.Measure.AddContent` `Mathlib.MeasureTheory.Measure.MeasureSpaceDef` `Mathlib.MeasureTheory.Measure.NullMeasurable` `Mathlib.MeasureTheory.OuterMeasure.Caratheodory` `Mathlib.MeasureTheory.OuterMeasure.Induced` `Mathlib.MeasureTheory.OuterMeasure.OfFunction` `Mathlib.NumberTheory.DiophantineApproximation.Basic` `Mathlib.NumberTheory.DiophantineApproximation.ContinuedFractions` `Mathlib.NumberTheory.Rayleigh` `Mathlib.RingTheory.MvPowerSeries.LinearTopology` `Mathlib.RingTheory.MvPowerSeries.PiTopology` `Mathlib.Topology.Baire.CompleteMetrizable` `Mathlib.Topology.GDelta.MetrizableSpace` `Mathlib.Topology.GDelta.UniformSpace` `Mathlib.Topology.MetricSpace.CantorScheme` `Mathlib.Topology.MetricSpace.Closeds` `Mathlib.Topology.MetricSpace.Contracting` `Mathlib.Topology.MetricSpace.HausdorffDistance` `Mathlib.Topology.MetricSpace.Perfect` `Mathlib.Topology.MetricSpace.PiNat` `Mathlib.Topology.MetricSpace.Polish` `Mathlib.Topology.MetricSpace.ThickenedIndicator` `Mathlib.Topology.MetricSpace.Thickening`	25
6 files `Mathlib.Algebra.Polynomial.GroupRingAction` `Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity` `Mathlib.NumberTheory.FLT.Polynomial` `Mathlib.RingTheory.Artinian.Algebra` `Mathlib.RingTheory.FractionalIdeal.Inverse` `Mathlib.RingTheory.FractionalIdeal.Operations`	26
32 files `Mathlib.Algebra.AlgebraicCard` `Mathlib.Algebra.Category.ContinuousCohomology.Basic` `Mathlib.Algebra.Category.FGModuleCat.Abelian` `Mathlib.Algebra.Category.FGModuleCat.Basic` `Mathlib.Algebra.Category.FGModuleCat.Colimits` `Mathlib.Algebra.Category.FGModuleCat.EssentiallySmall` `Mathlib.Algebra.Category.FGModuleCat.Limits` `Mathlib.Algebra.Category.ModuleCat.Topology.Basic` `Mathlib.Algebra.Category.ModuleCat.Topology.Homology` `Mathlib.Algebra.CharP.LocalRing` `Mathlib.Algebra.CharP.MixedCharZero` `Mathlib.Algebra.Polynomial.Expand` `Mathlib.Analysis.Convex.BetweenList` `Mathlib.Analysis.Convex.Between` `Mathlib.Analysis.Convex.Visible` `Mathlib.Analysis.Normed.Affine.ContinuousAffineMap` `Mathlib.FieldTheory.Minpoly.Basic` `Mathlib.LinearAlgebra.BilinearForm.DualLattice` `Mathlib.LinearAlgebra.BilinearForm.Orthogonal` `Mathlib.LinearAlgebra.BilinearForm.Properties` `Mathlib.LinearAlgebra.BilinearForm.TensorProduct` `Mathlib.LinearAlgebra.Coevaluation` `Mathlib.LinearAlgebra.Contraction` `Mathlib.LinearAlgebra.Dual.Lemmas` `Mathlib.LinearAlgebra.PerfectPairing.Basic` `Mathlib.RepresentationTheory.Basic` `Mathlib.RepresentationTheory.Submodule` `Mathlib.RingTheory.Algebraic.Basic` `Mathlib.RingTheory.Algebraic.MvPolynomial` `Mathlib.RingTheory.AlgebraicIndependent.Transcendental` `Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic` `Mathlib.Topology.Algebra.Module.ModuleTopology`	28
4 files `Mathlib.Analysis.Convex.Radon` `Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional` `Mathlib.RingTheory.LocalProperties.Projective` `Mathlib.RingTheory.Localization.Free`	30
29 files `Mathlib.Algebra.Algebra.Subalgebra.IsSimpleOrder` `Mathlib.Algebra.Algebra.Subalgebra.Rank` `Mathlib.Algebra.Lie.Sl2` `Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf` `Mathlib.Analysis.NormedSpace.Alternating.Basic` `Mathlib.Analysis.NormedSpace.Alternating.Curry` `Mathlib.CategoryTheory.Preadditive.HomOrthogonal` `Mathlib.LinearAlgebra.FreeAlgebra` `Mathlib.LinearAlgebra.FreeModule.Finite.Matrix` `Mathlib.LinearAlgebra.Matrix.FiniteDimensional` `Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber` `Mathlib.LinearAlgebra.Multilinear.FiniteDimensional` `Mathlib.LinearAlgebra.SymmetricAlgebra.Basis` `Mathlib.LinearAlgebra.TensorAlgebra.Basis` `Mathlib.NumberTheory.FrobeniusNumber` `Mathlib.RingTheory.Finiteness.Quotient` `Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization` `Mathlib.RingTheory.Ideal.NatInt` `Mathlib.RingTheory.KrullDimension.NonZeroDivisors` `Mathlib.RingTheory.LocalProperties.Basic` `Mathlib.RingTheory.LocalProperties.Reduced` `Mathlib.RingTheory.Localization.Finiteness` `Mathlib.RingTheory.MvPolynomial` `Mathlib.RingTheory.RingHom.FiniteType` `Mathlib.RingTheory.RingHom.Finite` `Mathlib.RingTheory.RingHom.Locally` `Mathlib.RingTheory.RingHom.OpenImmersion` `Mathlib.RingTheory.RingHom.Surjective` `Mathlib.RingTheory.Support`	31
62 files `Mathlib.Algebra.Category.CommAlgCat.FiniteType` `Mathlib.Algebra.Category.Ring.FinitePresentation` `Mathlib.Algebra.MvPolynomial.Nilpotent` `Mathlib.Analysis.Asymptotics.TVS` `Mathlib.Analysis.BoxIntegral.Partition.Additive` `Mathlib.Analysis.Calculus.FDeriv.Defs` `Mathlib.Analysis.Calculus.FormalMultilinearSeries` `Mathlib.Analysis.LocallyConvex.Barrelled` `Mathlib.Analysis.LocallyConvex.WithSeminorms` `Mathlib.Analysis.Normed.Algebra.Unitization` `Mathlib.Analysis.Normed.Field.WithAbs` `Mathlib.Analysis.Normed.Module.Completion` `Mathlib.Analysis.Normed.Operator.Asymptotics` `Mathlib.Analysis.Normed.Operator.Basic` `Mathlib.Analysis.Normed.Operator.Bilinear` `Mathlib.Analysis.Normed.Operator.Completeness` `Mathlib.Analysis.Normed.Operator.Mul` `Mathlib.Analysis.Normed.Operator.NNNorm` `Mathlib.Analysis.Normed.Operator.NormedSpace` `Mathlib.Analysis.Normed.Operator.Prod` `Mathlib.Analysis.NormedSpace.Multilinear.Basic` `Mathlib.Analysis.NormedSpace.Multilinear.Curry` `Mathlib.Analysis.NormedSpace.OperatorNorm.Asymptotics` `Mathlib.Analysis.NormedSpace.OperatorNorm.Basic` `Mathlib.Analysis.NormedSpace.OperatorNorm.Bilinear` `Mathlib.Analysis.NormedSpace.OperatorNorm.Completeness` `Mathlib.Analysis.NormedSpace.OperatorNorm.Mul` `Mathlib.Analysis.NormedSpace.OperatorNorm.NNNorm` `Mathlib.Analysis.NormedSpace.OperatorNorm.NormedSpace` `Mathlib.Analysis.NormedSpace.OperatorNorm.Prod` `Mathlib.Analysis.NormedSpace.PiTensorProduct.InjectiveSeminorm` `Mathlib.Analysis.NormedSpace.PiTensorProduct.ProjectiveSeminorm` `Mathlib.Dynamics.Newton` `Mathlib.GroupTheory.CosetCover` `Mathlib.LinearAlgebra.FreeModule.StrongRankCondition` `Mathlib.RingTheory.AdicCompletion.Noetherian` `Mathlib.RingTheory.Artinian.Instances` `Mathlib.RingTheory.Derivation.Lie` `Mathlib.RingTheory.DividedPowers.SubDPIdeal` `Mathlib.RingTheory.EssentialFiniteness` `Mathlib.RingTheory.Filtration` `Mathlib.RingTheory.FinitePresentation` `Mathlib.RingTheory.FiniteStability` `Mathlib.RingTheory.FiniteType` `Mathlib.RingTheory.Finiteness.Small` `Mathlib.RingTheory.FractionalIdeal.Basic` `Mathlib.RingTheory.FractionalIdeal.Extended` `Mathlib.RingTheory.GradedAlgebra.FiniteType` `Mathlib.RingTheory.Henselian` `Mathlib.RingTheory.Jacobson.Polynomial` `Mathlib.RingTheory.Localization.Away.Lemmas` `Mathlib.RingTheory.Localization.InvSubmonoid` `Mathlib.RingTheory.Localization.Submodule` `Mathlib.RingTheory.Polynomial.IrreducibleRing` `Mathlib.RingTheory.Polynomial.Nilpotent` `Mathlib.RingTheory.Polynomial.Quotient` `Mathlib.RingTheory.PowerSeries.WeierstrassPreparation` `Mathlib.RingTheory.ReesAlgebra` `Mathlib.Topology.Category.DeltaGenerated` `Mathlib.Topology.Compactness.DeltaGeneratedSpace` `Mathlib.Topology.ContinuousMap.Bounded.Normed` `Mathlib.Topology.ContinuousMap.BoundedCompactlySupported`	32
59 files `Mathlib.Algebra.Category.ModuleCat.Free` `Mathlib.Algebra.Category.ModuleCat.Simple` `Mathlib.Algebra.Category.Ring.Topology` `Mathlib.Algebra.DualQuaternion` `Mathlib.Algebra.LinearRecurrence` `Mathlib.Algebra.Module.Lattice` `Mathlib.Algebra.Module.SpanRank` `Mathlib.Algebra.QuadraticAlgebra` `Mathlib.Algebra.QuaternionBasis` `Mathlib.Algebra.Quaternion` `Mathlib.Analysis.Asymptotics.AsymptoticEquivalent` `Mathlib.Analysis.Asymptotics.Completion` `Mathlib.Analysis.Asymptotics.Lemmas` `Mathlib.Analysis.Asymptotics.SuperpolynomialDecay` `Mathlib.Analysis.Asymptotics.Theta` `Mathlib.Analysis.Normed.Algebra.Ultra` `Mathlib.Analysis.Normed.Field.Ultra` `Mathlib.Analysis.Normed.Group.FunctionSeries` `Mathlib.Analysis.Normed.Group.InfiniteSum` `Mathlib.Analysis.Normed.Group.Ultra` `Mathlib.Analysis.Normed.Ring.InfiniteSum` `Mathlib.Analysis.Normed.Ring.Ultra` `Mathlib.Analysis.NormedSpace.FunctionSeries` `Mathlib.FieldTheory.Finiteness` `Mathlib.GroupTheory.FreeGroup.GeneratorEquiv` `Mathlib.LinearAlgebra.Basis.MulOpposite` `Mathlib.LinearAlgebra.Dimension.Constructions` `Mathlib.LinearAlgebra.Dimension.DivisionRing` `Mathlib.LinearAlgebra.Dimension.ErdosKaplansky` `Mathlib.LinearAlgebra.Dimension.Finite` `Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition` `Mathlib.LinearAlgebra.Dimension.Free` `Mathlib.LinearAlgebra.Dimension.LinearMap` `Mathlib.LinearAlgebra.Dimension.Localization` `Mathlib.LinearAlgebra.Dimension.RankNullity` `Mathlib.LinearAlgebra.Dimension.StrongRankCondition` `Mathlib.LinearAlgebra.Eigenspace.Basic` `Mathlib.LinearAlgebra.Eigenspace.Matrix` `Mathlib.LinearAlgebra.FiniteDimensional.Basic` `Mathlib.LinearAlgebra.FiniteDimensional.Defs` `Mathlib.LinearAlgebra.FiniteDimensional.Lemmas` `Mathlib.LinearAlgebra.FreeModule.PID` `Mathlib.LinearAlgebra.Matrix.Diagonal` `Mathlib.LinearAlgebra.Projectivization.Action` `Mathlib.LinearAlgebra.Projectivization.Basic` `Mathlib.LinearAlgebra.Projectivization.Independence` `Mathlib.LinearAlgebra.Projectivization.Subspace` `Mathlib.Order.Filter.ZeroAndBoundedAtFilter` `Mathlib.RingTheory.Adjoin.Dimension` `Mathlib.RingTheory.Length` `Mathlib.RingTheory.LocalRing.ResidueField.Fiber` `Mathlib.RingTheory.LocalRing.ResidueField.Ideal` `Mathlib.RingTheory.SimpleModule.Rank` `Mathlib.RingTheory.Spectrum.Maximal.Localization` `Mathlib.RingTheory.Spectrum.Prime.RingHom` `Mathlib.RingTheory.Valuation.Extension` `Mathlib.RingTheory.Valuation.RamificationGroup` `Mathlib.RingTheory.Valuation.ValExtension` `Mathlib.RingTheory.Valuation.ValuationSubring`	33
49 files `Mathlib.Algebra.Jordan.Basic` `Mathlib.Algebra.Lie.Abelian` `Mathlib.Algebra.Lie.BaseChange` `Mathlib.Algebra.Lie.CartanMatrix` `Mathlib.Algebra.Lie.Derivation.AdjointAction` `Mathlib.Algebra.Lie.Derivation.Basic` `Mathlib.Algebra.Lie.DirectSum` `Mathlib.Algebra.Lie.Extension` `Mathlib.Algebra.Lie.Free` `Mathlib.Algebra.Lie.IdealOperations` `Mathlib.Algebra.Lie.Ideal` `Mathlib.Algebra.Lie.Normalizer` `Mathlib.Algebra.Lie.OfAssociative` `Mathlib.Algebra.Lie.Quotient` `Mathlib.Algebra.Lie.Subalgebra` `Mathlib.Algebra.Lie.Submodule` `Mathlib.Algebra.Lie.TensorProduct` `Mathlib.Algebra.Lie.UniversalEnveloping` `Mathlib.Algebra.Module.FinitePresentation` `Mathlib.Algebra.Module.Presentation.Finite` `Mathlib.Algebra.Symmetrized` `Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField` `Mathlib.LinearAlgebra.InvariantBasisNumber` `Mathlib.NumberTheory.BernoulliPolynomials` `Mathlib.NumberTheory.Bernoulli` `Mathlib.RingTheory.Adjoin.FG` `Mathlib.RingTheory.Adjoin.Tower` `Mathlib.RingTheory.AlgebraicIndependent.Basic` `Mathlib.RingTheory.Artinian.Module` `Mathlib.RingTheory.Artinian.Ring` `Mathlib.RingTheory.Derivation.ToSquareZero` `Mathlib.RingTheory.EisensteinCriterion` `Mathlib.RingTheory.FiniteLength` `Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness` `Mathlib.RingTheory.Ideal.Quotient.Nilpotent` `Mathlib.RingTheory.Ideal.Quotient.Noetherian` `Mathlib.RingTheory.LocalRing.ResidueField.Basic` `Mathlib.RingTheory.Localization.Algebra` `Mathlib.RingTheory.MvPolynomial.Localization` `Mathlib.RingTheory.Polynomial.Basic` `Mathlib.RingTheory.Polynomial.ContentIdeal` `Mathlib.RingTheory.Polynomial.Eisenstein.Basic` `Mathlib.RingTheory.Polynomial.Eisenstein.Criterion` `Mathlib.RingTheory.Polynomial.Eisenstein.Distinguished` `Mathlib.RingTheory.Polynomial.UniqueFactorization` `Mathlib.RingTheory.PowerSeries.Derivative` `Mathlib.RingTheory.PowerSeries.Inverse` `Mathlib.RingTheory.SimpleModule.WedderburnArtin` `Mathlib.RingTheory.TensorProduct.DirectLimitFG`	34
13 files `Mathlib.RingTheory.Ideal.AssociatedPrime.Localization` `Mathlib.RingTheory.Ideal.MinimalPrime.Localization` `Mathlib.RingTheory.Ideal.Over` `Mathlib.RingTheory.LocalProperties.Exactness` `Mathlib.RingTheory.LocalProperties.Submodule` `Mathlib.RingTheory.LocalRing.LocalSubring` `Mathlib.RingTheory.Localization.AsSubring` `Mathlib.RingTheory.Localization.AtPrime.Basic` `Mathlib.RingTheory.Localization.AtPrime` `Mathlib.RingTheory.Localization.LocalizationLocalization` `Mathlib.RingTheory.SimpleModule.InjectiveProjective` `Mathlib.RingTheory.SurjectiveOnStalks` `Mathlib.Topology.Algebra.InfiniteSum.Module`	35
43 files `Mathlib.Algebra.Category.CommAlgCat.Basic` `Mathlib.Algebra.Category.CommAlgCat.Monoidal` `Mathlib.Algebra.Category.CommBialgCat` `Mathlib.Algebra.Category.Ring.Constructions` `Mathlib.Algebra.Category.Ring.Epi` `Mathlib.Algebra.Category.Ring.Instances` `Mathlib.Algebra.Category.Ring.Under.Basic` `Mathlib.Algebra.DirectSum.Idempotents` `Mathlib.Algebra.Homology.LocalCohomology` `Mathlib.FieldTheory.Tower` `Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits` `Mathlib.Geometry.RingedSpace.LocallyRingedSpace` `Mathlib.Geometry.RingedSpace.OpenImmersion` `Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing` `Mathlib.LinearAlgebra.Matrix.Ideal` `Mathlib.RingTheory.AdicCompletion.Basic` `Mathlib.RingTheory.AdicCompletion.LocalRing` `Mathlib.RingTheory.DiscreteValuationRing.Basic` `Mathlib.RingTheory.DualNumber` `Mathlib.RingTheory.GradedAlgebra.Noetherian` `Mathlib.RingTheory.Ideal.AssociatedPrime.Basic` `Mathlib.RingTheory.Ideal.AssociatedPrime` `Mathlib.RingTheory.Ideal.Quotient.Operations` `Mathlib.RingTheory.Idempotents` `Mathlib.RingTheory.Jacobson.Ideal` `Mathlib.RingTheory.KrullDimension.Basic` `Mathlib.RingTheory.KrullDimension.Field` `Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic` `Mathlib.RingTheory.LocalRing.NonLocalRing` `Mathlib.RingTheory.LocalRing.ResidueField.Defs` `Mathlib.RingTheory.LocalRing.RingHom.Basic` `Mathlib.RingTheory.Localization.Ideal` `Mathlib.RingTheory.MvPolynomial.Basic` `Mathlib.RingTheory.Nakayama` `Mathlib.RingTheory.Noetherian.Basic` `Mathlib.RingTheory.Noetherian.Orzech` `Mathlib.RingTheory.RingHom.Injective` `Mathlib.RingTheory.RingHomProperties` `Mathlib.RingTheory.SimpleRing.Matrix` `Mathlib.RingTheory.Spectrum.Prime.Basic` `Mathlib.RingTheory.TensorProduct.Finite` `Mathlib.RingTheory.TensorProduct.Quotient` `Mathlib.RingTheory.Valuation.Quotient`	36
9 files `Mathlib.NumberTheory.Harmonic.Int` `Mathlib.NumberTheory.Padics.PadicNumbers` `Mathlib.NumberTheory.Zsqrtd.ToReal` `Mathlib.RepresentationTheory.Maschke` `Mathlib.RingTheory.Jacobson.Semiprimary` `Mathlib.RingTheory.SimpleModule.Basic` `Mathlib.RingTheory.SimpleModule.Isotypic` `Mathlib.Topology.Algebra.Polynomial` `Mathlib.Topology.ContinuousMap.Polynomial`	37
5 files `Mathlib.Algebra.Azumaya.Matrix` `Mathlib.Algebra.FreeAlgebra.Cardinality` `Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient` `Mathlib.RingTheory.Regular.Category` `Mathlib.SetTheory.Cardinal.Free`	38
4 files `Mathlib.LinearAlgebra.FreeModule.Finite.Basic` `Mathlib.RingTheory.Finiteness.Cardinality` `Mathlib.RingTheory.Finiteness.Projective` `Mathlib.RingTheory.OrzechProperty`	43
`Mathlib.ModelTheory.Algebra.Field.CharP`	44
`Mathlib.LinearAlgebra.Alternating.DomCoprod`	45
8 files `Mathlib.Algebra.MvPolynomial.Cardinal` `Mathlib.Algebra.Star.CHSH` `Mathlib.Analysis.Complex.Exponential` `Mathlib.Analysis.Complex.Trigonometric` `Mathlib.Analysis.SpecialFunctions.Log.ERealExp` `Mathlib.Data.Complex.Exponential` `Mathlib.Data.Complex.Trigonometric` `Mathlib.RingTheory.Algebraic.Cardinality`	47
4 files `Mathlib.Analysis.CStarAlgebra.Basic` `Mathlib.ModelTheory.Algebra.Ring.FreeCommRing` `Mathlib.RingTheory.Ideal.Quotient.Basic` `Mathlib.Topology.Sheaves.MayerVietoris`	49
11 files `Mathlib.Algebra.Polynomial.Homogenize` `Mathlib.CategoryTheory.Sites.MayerVietorisSquare` `Mathlib.Combinatorics.Nullstellensatz` `Mathlib.NumberTheory.FLT.MasonStothers` `Mathlib.RingTheory.MvPolynomial.EulerIdentity` `Mathlib.RingTheory.MvPolynomial.Groebner` `Mathlib.RingTheory.MvPolynomial.Homogeneous` `Mathlib.RingTheory.MvPolynomial.MonomialOrder.DegLex` `Mathlib.RingTheory.MvPolynomial.MonomialOrder` `Mathlib.RingTheory.Polynomial.Radical` `Mathlib.Topology.Algebra.InfiniteSum.ENNReal`	50
27 files `Mathlib.Algebra.Category.Grp.IsFinite` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification` `Mathlib.Algebra.Category.ModuleCat.Sheaf.Abelian` `Mathlib.Algebra.Category.ModuleCat.Sheaf.Colimits` `Mathlib.Algebra.Category.ModuleCat.Sheaf.Free` `Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators` `Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous` `Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent` `Mathlib.Algebra.Homology.ConcreteCategory` `Mathlib.Analysis.Complex.Norm` `Mathlib.Analysis.Complex.Order` `Mathlib.CategoryTheory.Abelian.Ext` `Mathlib.Data.Rat.NatSqrt.Real` `Mathlib.Data.Real.CompleteField` `Mathlib.Data.Real.Sqrt` `Mathlib.Data.Real.StarOrdered` `Mathlib.MeasureTheory.OuterMeasure.AE` `Mathlib.MeasureTheory.OuterMeasure.Basic` `Mathlib.MeasureTheory.OuterMeasure.BorelCantelli` `Mathlib.MeasureTheory.OuterMeasure.Operations` `Mathlib.Tactic.NormNum.RealSqrt` `Mathlib.Topology.Algebra.InfiniteSum.Real` `Mathlib.Topology.EMetricSpace.BoundedVariation` `Mathlib.Topology.Instances.ENNReal.Lemmas` `Mathlib.Topology.Instances.EReal.Lemmas` `Mathlib.Topology.Instances.NNReal.Lemmas` `Mathlib.Topology.Semicontinuous`	51
20 files `Mathlib.Algebra.Category.Grp.AB` `Mathlib.Algebra.Category.Grp.Abelian` `Mathlib.Algebra.Category.Grp.Images` `Mathlib.Algebra.Category.ModuleCat.AB` `Mathlib.Algebra.Category.ModuleCat.Abelian` `Mathlib.Algebra.Category.ModuleCat.Biproducts` `Mathlib.Algebra.Category.ModuleCat.Images` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Abelian` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback` `Mathlib.Algebra.Homology.ShortComplex.Ab` `Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory` `Mathlib.Algebra.Homology.ShortComplex.ModuleCat` `Mathlib.CategoryTheory.Abelian.FreydMitchell` `Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu` `Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite` `Mathlib.CategoryTheory.Abelian.Injective.Basic` `Mathlib.CategoryTheory.Abelian.Projective.Basic` `Mathlib.CategoryTheory.Abelian.Yoneda` `Mathlib.CategoryTheory.Preadditive.Yoneda.Limits`	52
4 files `Mathlib.Analysis.Normed.Affine.Isometry` `Mathlib.Analysis.Normed.Affine.MazurUlam` `Mathlib.Topology.Algebra.Module.Alternating.Topology` `Mathlib.Topology.Algebra.Module.CharacterSpace`	53
8 files `Mathlib.Analysis.LocallyConvex.StrongTopology` `Mathlib.Analysis.Normed.Operator.Compact` `Mathlib.Topology.Algebra.InfiniteSum.Order` `Mathlib.Topology.Algebra.Module.Multilinear.Topology` `Mathlib.Topology.Algebra.Module.StrongTopology` `Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology` `Mathlib.Topology.CWComplex.Classical.Basic` `Mathlib.Topology.CWComplex.Classical.Finite`	54
17 files `Mathlib.Algebra.Polynomial.Degree.CardPowDegree` `Mathlib.Analysis.LocallyConvex.AbsConvex` `Mathlib.Analysis.LocallyConvex.Bounded` `Mathlib.Analysis.Normed.Affine.AddTorsor` `Mathlib.Analysis.Normed.Module.Ball.Action` `Mathlib.Analysis.Normed.Module.Ball.RadialEquiv` `Mathlib.Analysis.Normed.Module.RCLike.Real` `Mathlib.Analysis.Normed.Module.Ray` `Mathlib.Analysis.Normed.Module.Span` `Mathlib.Analysis.NormedSpace.BallAction` `Mathlib.Analysis.NormedSpace.ConformalLinearMap` `Mathlib.Analysis.NormedSpace.ENormedSpace` `Mathlib.Analysis.NormedSpace.Extr` `Mathlib.Analysis.NormedSpace.Real` `Mathlib.Analysis.NormedSpace.SphereNormEquiv` `Mathlib.Topology.Algebra.Module.Multilinear.Bounded` `Mathlib.Topology.Algebra.Module.UniformConvergence`	55
14 files `Mathlib.Algebra.CubicDiscriminant` `Mathlib.Algebra.Polynomial.Splits` `Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ` `Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms` `Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange` `Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass` `Mathlib.Analysis.Convex.Topology` `Mathlib.Analysis.Convex.TotallyBounded` `Mathlib.Analysis.Normed.Group.SemiNormedGrp.Completion` `Mathlib.Analysis.Normed.Group.SemiNormedGrp` `Mathlib.RingTheory.Polynomial.SmallDegreeVieta` `Mathlib.RingTheory.Polynomial.Vieta` `Mathlib.Topology.Algebra.Module.LocallyConvex` `Mathlib.Topology.ContinuousMap.LocallyConvex`	56
12 files `Mathlib.Algebra.Polynomial.FieldDivision` `Mathlib.Algebra.Polynomial.SpecificDegree` `Mathlib.Analysis.Convex.EGauge` `Mathlib.Analysis.LocallyConvex.BalancedCoreHull` `Mathlib.Analysis.LocallyConvex.Basic` `Mathlib.Analysis.LocallyConvex.Polar` `Mathlib.Analysis.Normed.Operator.ContinuousLinearMap` `Mathlib.Analysis.Normed.Operator.LinearIsometry` `Mathlib.Analysis.Seminorm` `Mathlib.RingTheory.Polynomial.Content` `Mathlib.RingTheory.Polynomial.Eisenstein.Generalized` `Mathlib.Topology.Algebra.Module.StrongDual`	57
27 files `Mathlib.Analysis.Normed.Field.Instances` `Mathlib.Analysis.Normed.Field.Lemmas` `Mathlib.Analysis.Normed.Field.UnitBall` `Mathlib.Analysis.Normed.Group.BallSphere` `Mathlib.Analysis.Normed.Group.Completion` `Mathlib.Analysis.Normed.Group.HomCompletion` `Mathlib.Analysis.Normed.Group.Hom` `Mathlib.Analysis.Normed.Group.Lemmas` `Mathlib.Analysis.Normed.Group.NullSubmodule` `Mathlib.Analysis.Normed.Group.SeparationQuotient` `Mathlib.Analysis.Normed.Group.Uniform` `Mathlib.Analysis.Normed.Module.Basic` `Mathlib.Analysis.Normed.MulAction` `Mathlib.Analysis.Normed.Order.Lattice` `Mathlib.Analysis.Normed.Ring.Int` `Mathlib.Analysis.Normed.Ring.Lemmas` `Mathlib.Analysis.NormedSpace.Int` `Mathlib.RingTheory.Polynomial.HilbertPoly` `Mathlib.Topology.Algebra.Algebra.Equiv` `Mathlib.Topology.Algebra.Algebra` `Mathlib.Topology.Algebra.StarSubalgebra` `Mathlib.Topology.Algebra.TopologicallyNilpotent` `Mathlib.Topology.Bornology.BoundedOperation` `Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli` `Mathlib.Topology.ContinuousMap.Bounded.Basic` `Mathlib.Topology.Instances.TrivSqZeroExt` `Mathlib.Topology.UniformSpace.Dini`	59
5 files `Mathlib.Algebra.MvPolynomial.SchwartzZippel` `Mathlib.RingTheory.HahnSeries.PowerSeries` `Mathlib.Topology.Instances.RealVectorSpace` `Mathlib.Topology.MetricSpace.Algebra` `Mathlib.Topology.MetricSpace.Completion`	60
4 files `Mathlib.Algebra.MvPolynomial.Funext` `Mathlib.Algebra.Polynomial.Roots` `Mathlib.Topology.Algebra.SeparationQuotient.FiniteDimensional` `Mathlib.Topology.Algebra.SeparationQuotient.Section`	61
`Mathlib.Analysis.CStarAlgebra.Module.Synonym`	62
`Mathlib.RingTheory.MvPowerSeries.Inverse`	64
`Mathlib.Analysis.Convex.Cone.Basic` `Mathlib.Analysis.Convex.Exposed`	65
10 files `Mathlib.Analysis.Normed.Affine.Simplex` `Mathlib.RingTheory.Bialgebra.MonoidAlgebra` `Mathlib.RingTheory.Coalgebra.MonoidAlgebra` `Mathlib.RingTheory.Finiteness.Nilpotent` `Mathlib.RingTheory.HopfAlgebra.MonoidAlgebra` `Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors` `Mathlib.RingTheory.Nilpotent.Lemmas` `Mathlib.RingTheory.Noetherian.Nilpotent` `Mathlib.Topology.Algebra.IntermediateField` `Mathlib.Topology.Algebra.Nonarchimedean.Bases`	66
9 files `Mathlib.Algebra.Colimit.Ring` `Mathlib.Analysis.Convex.StdSimplex` `Mathlib.LinearAlgebra.AffineSpace.ContinuousAffineEquiv` `Mathlib.RingTheory.Polynomial.GaussNorm` `Mathlib.RingTheory.PowerSeries.GaussNorm` `Mathlib.Topology.Algebra.AffineSubspace` `Mathlib.Topology.Algebra.ContinuousAffineMap` `Mathlib.Topology.Algebra.Module.Alternating.Basic` `Mathlib.Topology.ContinuousMap.LocallyConstant`	67
17 files `Mathlib.NumberTheory.Zsqrtd.GaussianInt` `Mathlib.Topology.Algebra.Group.CompactOpen` `Mathlib.Topology.Algebra.Module.ClosedSubmodule` `Mathlib.Topology.Algebra.Module.Equiv` `Mathlib.Topology.Algebra.Module.LinearMapPiProd` `Mathlib.Topology.Algebra.Module.LinearMap` `Mathlib.Topology.Algebra.Module.Multilinear.Basic` `Mathlib.Topology.Algebra.Module.PerfectPairing` `Mathlib.Topology.Algebra.Module.Star` `Mathlib.Topology.Algebra.Module.WeakBilin` `Mathlib.Topology.Algebra.Module.WeakDual` `Mathlib.Topology.Algebra.SeparationQuotient.Basic` `Mathlib.Topology.Algebra.SeparationQuotient.Hom` `Mathlib.Topology.ContinuousMap.Algebra` `Mathlib.Topology.ContinuousMap.Lattice` `Mathlib.Topology.ContinuousMap.Star` `Mathlib.Topology.UniformSpace.ProdApproximation`	68
17 files `Mathlib.Algebra.Polynomial.Derivation` `Mathlib.Algebra.Polynomial.Module.AEval` `Mathlib.Algebra.Polynomial.Module.Basic` `Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology` `Mathlib.Analysis.Convex.PathConnected` `Mathlib.LinearAlgebra.Complex.Module` `Mathlib.NumberTheory.Dioph` `Mathlib.NumberTheory.PellMatiyasevic` `Mathlib.RingTheory.Finiteness.Ideal` `Mathlib.RingTheory.FreeCommRing` `Mathlib.RingTheory.MvPolynomial.FreeCommRing` `Mathlib.Topology.Algebra.FilterBasis` `Mathlib.Topology.Algebra.Module.Basic` `Mathlib.Topology.Algebra.Module.LinearPMap` `Mathlib.Topology.Algebra.NonUnitalAlgebra` `Mathlib.Topology.Algebra.NonUnitalStarAlgebra` `Mathlib.Topology.Algebra.UniformFilterBasis`	69
8 files `Mathlib.Algebra.Order.Ring.Archimedean` `Mathlib.Algebra.Polynomial.Laurent` `Mathlib.LinearAlgebra.TensorProduct.Vanishing` `Mathlib.RingTheory.Int.Basic` `Mathlib.RingTheory.Polynomial.Ideal` `Mathlib.RingTheory.PowerSeries.NoZeroDivisors` `Mathlib.RingTheory.PowerSeries.Order` `Mathlib.RingTheory.QuotSMulTop`	70
16 files `Mathlib.Algebra.Polynomial.CoeffMem` `Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree` `Mathlib.Algebra.Polynomial.Lifts` `Mathlib.Algebra.Polynomial.RingDivision` `Mathlib.Algebra.Polynomial.SumIteratedDerivative` `Mathlib.Algebra.Polynomial.Taylor` `Mathlib.NumberTheory.FLT.Basic` `Mathlib.RingTheory.DividedPowers.Basic` `Mathlib.RingTheory.DividedPowers.DPMorphism` `Mathlib.RingTheory.DividedPowers.RatAlgebra` `Mathlib.RingTheory.Jacobson.Radical` `Mathlib.RingTheory.Lasker` `Mathlib.RingTheory.Localization.BaseChange` `Mathlib.RingTheory.Polynomial.IntegralNormalization` `Mathlib.RingTheory.TensorProduct.IsBaseChangePi` `Mathlib.RingTheory.Valuation.PrimeMultiplicity`	71
16 files `Mathlib.Combinatorics.SimpleGraph.AdjMatrix` `Mathlib.Combinatorics.SimpleGraph.StronglyRegular` `Mathlib.LinearAlgebra.TensorProduct.Quotient` `Mathlib.LinearAlgebra.TensorProduct.RightExactness` `Mathlib.RingTheory.Ideal.IsPrimary` `Mathlib.RingTheory.Ideal.MinimalPrime.Basic` `Mathlib.RingTheory.Ideal.Quotient.PowTransition` `Mathlib.RingTheory.IsPrimary` `Mathlib.RingTheory.Localization.Away.Basic` `Mathlib.RingTheory.Polynomial.Bernstein` `Mathlib.RingTheory.Polynomial.Wronskian` `Mathlib.RingTheory.TensorProduct.MvPolynomial` `Mathlib.RingTheory.Valuation.ValuationRing` `Mathlib.RingTheory.Valuation.ValuativeRel.Basic` `Mathlib.RingTheory.Valuation.ValuativeRel` `Mathlib.Topology.Algebra.Star.Unitary`	72
22 files `Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic` `Mathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup` `Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps` `Mathlib.AlgebraicTopology.FundamentalGroupoid.PUnit` `Mathlib.AlgebraicTopology.FundamentalGroupoid.Product` `Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected` `Mathlib.NumberTheory.Zsqrtd.Basic` `Mathlib.RingTheory.Bezout` `Mathlib.RingTheory.EuclideanDomain` `Mathlib.RingTheory.HahnSeries.HEval` `Mathlib.RingTheory.Ideal.IsPrincipal` `Mathlib.RingTheory.MvPowerSeries.LexOrder` `Mathlib.RingTheory.Noetherian.UniqueFactorizationDomain` `Mathlib.RingTheory.PowerSeries.Basic` `Mathlib.RingTheory.PowerSeries.CoeffMulMem` `Mathlib.RingTheory.PowerSeries.Trunc` `Mathlib.RingTheory.PowerSeries.WellKnown` `Mathlib.RingTheory.PrincipalIdealDomainOfPrime` `Mathlib.RingTheory.PrincipalIdealDomain` `Mathlib.RingTheory.SimpleRing.Principal` `Mathlib.Topology.Homotopy.HomotopyGroup` `Mathlib.Topology.Homotopy.Lifting`	73
27 files `Mathlib.Algebra.Azumaya.Basic` `Mathlib.Algebra.Azumaya.Defs` `Mathlib.Algebra.CharP.IntermediateField` `Mathlib.Algebra.MvPolynomial.Derivation` `Mathlib.Algebra.MvPolynomial.Equiv` `Mathlib.Algebra.MvPolynomial.PDeriv` `Mathlib.Algebra.MvPolynomial.Polynomial` `Mathlib.Algebra.Polynomial.AlgebraMap` `Mathlib.Algebra.Polynomial.Smeval` `Mathlib.Algebra.Ring.Subring.IntPolynomial` `Mathlib.FieldTheory.IntermediateField.Adjoin.Defs` `Mathlib.FieldTheory.IntermediateField.Basic` `Mathlib.RingTheory.Adjoin.Polynomial` `Mathlib.RingTheory.Algebraic.Defs` `Mathlib.RingTheory.Algebraic.LinearIndependent` `Mathlib.RingTheory.Algebraic.Pi` `Mathlib.RingTheory.Derivation.Basic` `Mathlib.RingTheory.Derivation.DifferentialRing` `Mathlib.RingTheory.Finiteness.Nakayama` `Mathlib.RingTheory.Ideal.Colon` `Mathlib.RingTheory.Ideal.IdempotentFG` `Mathlib.RingTheory.Ideal.Oka` `Mathlib.RingTheory.Polynomial.ScaleRoots` `Mathlib.RingTheory.Polynomial.ShiftedLegendre` `Mathlib.RingTheory.Polynomial.Tower` `Mathlib.RingTheory.PolynomialAlgebra` `Mathlib.Topology.Algebra.MvPolynomial`	74
11 files `Mathlib.Algebra.Algebra.Subalgebra.Centralizer` `Mathlib.LinearAlgebra.Dimension.Basic` `Mathlib.LinearAlgebra.Dimension.Finrank` `Mathlib.LinearAlgebra.Dimension.Subsingleton` `Mathlib.LinearAlgebra.Matrix.Dual` `Mathlib.LinearAlgebra.Matrix.ToLin` `Mathlib.RingTheory.Coprime.Ideal` `Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal` `Mathlib.RingTheory.GradedAlgebra.Radical` `Mathlib.RingTheory.TensorProduct.Free` `Mathlib.Topology.Algebra.InfiniteSum.Field`	75
14 files `Mathlib.Algebra.Category.AlgCat.Limits` `Mathlib.Algebra.Category.BialgCat.Basic` `Mathlib.Algebra.Category.BialgCat.Monoidal` `Mathlib.Algebra.Category.HopfAlgCat.Basic` `Mathlib.Algebra.Category.HopfAlgCat.Monoidal` `Mathlib.Analysis.Convex.Contractible` `Mathlib.RingTheory.HahnSeries.Valuation` `Mathlib.RingTheory.MvPowerSeries.Order` `Mathlib.RingTheory.Valuation.Basic` `Mathlib.RingTheory.Valuation.ExtendToLocalization` `Mathlib.RingTheory.Valuation.Integers` `Mathlib.Topology.Homotopy.Contractible` `Mathlib.Topology.Homotopy.Path` `Mathlib.Topology.Homotopy.Product`	76
10 files `Mathlib.Algebra.Algebra.Spectrum.Basic` `Mathlib.Algebra.Algebra.Spectrum.Pi` `Mathlib.Algebra.Algebra.Spectrum.Quasispectrum` `Mathlib.Algebra.Algebra.Subalgebra.Operations` `Mathlib.Algebra.Star.Unitary` `Mathlib.RingTheory.Ideal.Maps` `Mathlib.RingTheory.Ideal.Operations` `Mathlib.RingTheory.Ideal.Pointwise` `Mathlib.RingTheory.Ideal.Prod` `Mathlib.RingTheory.UniqueFactorizationDomain.Ideal`	77
6 files `Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify` `Mathlib.Algebra.Category.ModuleCat.Sheaf.ChangeOfRings` `Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits` `Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous` `Mathlib.Algebra.Category.ModuleCat.Sheaf` `Mathlib.RingTheory.Nilpotent.Exp`	78
12 files `Mathlib.Combinatorics.Additive.ApproximateSubgroup` `Mathlib.LinearAlgebra.FreeProduct.Basic` `Mathlib.LinearAlgebra.TensorAlgebra.Grading` `Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower` `Mathlib.RingTheory.Bialgebra.Basic` `Mathlib.RingTheory.Bialgebra.Equiv` `Mathlib.RingTheory.Bialgebra.Hom` `Mathlib.RingTheory.Bialgebra.TensorProduct` `Mathlib.RingTheory.HopfAlgebra.Basic` `Mathlib.RingTheory.HopfAlgebra.TensorProduct` `Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem` `Mathlib.Topology.Algebra.Module.Compact`	79
`Mathlib.AlgebraicTopology.SingularHomology.Basic` `Mathlib.Analysis.Polynomial.CauchyBound`	80
7 files `Mathlib.Algebra.Module.LocalizedModule.Submodule` `Mathlib.Analysis.Convex.Caratheodory` `Mathlib.Analysis.Convex.Combination` `Mathlib.Analysis.Convex.Independent` `Mathlib.Analysis.Convex.Jensen` `Mathlib.Analysis.Convex.SimplicialComplex.Basic` `Mathlib.Analysis.Convex.StoneSeparation`	81
13 files `Mathlib.Algebra.Category.CoalgCat.Basic` `Mathlib.Algebra.Category.CoalgCat.ComonEquivalence` `Mathlib.Algebra.Category.CoalgCat.Monoidal` `Mathlib.Algebra.Colimit.Finiteness` `Mathlib.Algebra.Colimit.TensorProduct` `Mathlib.Algebra.DirectSum.Internal` `Mathlib.Algebra.Module.GradedModule` `Mathlib.Algebra.MonoidAlgebra.Grading` `Mathlib.LinearAlgebra.TensorProduct.Subalgebra` `Mathlib.LinearAlgebra.TensorProduct.Submodule` `Mathlib.RingTheory.GradedAlgebra.Basic` `Mathlib.RingTheory.GradedAlgebra.Homogeneous.Submodule` `Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous`	82
6 files `Mathlib.Algebra.Category.ModuleCat.Projective` `Mathlib.Algebra.Module.Presentation.Free` `Mathlib.Analysis.Convex.Strict` `Mathlib.Analysis.Normed.Group.Bounded` `Mathlib.Analysis.Normed.Group.Continuity` `Mathlib.Analysis.Normed.Group.Rat`	83
17 files `Mathlib.Algebra.Category.ModuleCat.ChangeOfRings` `Mathlib.Algebra.Category.ModuleCat.Presheaf.ChangeOfRings` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits` `Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Free` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward` `Mathlib.Algebra.Category.ModuleCat.Presheaf` `Mathlib.Algebra.Category.ModuleCat.Pseudofunctor` `Mathlib.Algebra.CharP.Algebra` `Mathlib.Algebra.CharP.Subring` `Mathlib.LinearAlgebra.AffineSpace.Basis` `Mathlib.LinearAlgebra.AffineSpace.Independent` `Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic` `Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid` `Mathlib.RingTheory.Morita.Basic`	84
11 files `Mathlib.AlgebraicTopology.SingularSet` `Mathlib.AlgebraicTopology.TopologicalSimplex` `Mathlib.LinearAlgebra.DirectSum.Finite` `Mathlib.LinearAlgebra.TensorProduct.Finiteness` `Mathlib.RingTheory.Coalgebra.Basic` `Mathlib.RingTheory.Coalgebra.Equiv` `Mathlib.RingTheory.Coalgebra.Hom` `Mathlib.RingTheory.Coalgebra.MulOpposite` `Mathlib.RingTheory.Coalgebra.TensorProduct` `Mathlib.RingTheory.MvPowerSeries.Basic` `Mathlib.RingTheory.MvPowerSeries.Trunc`	85
4 files `Mathlib.Algebra.Group.UniqueProds.VectorSpace` `Mathlib.LinearAlgebra.SymmetricAlgebra.Basic` `Mathlib.LinearAlgebra.TensorAlgebra.Basic` `Mathlib.RingTheory.HahnSeries.Summable`	86
`Mathlib.Geometry.Convex.Cone.Dual` `Mathlib.RingTheory.Finiteness.Finsupp`	87
7 files `Mathlib.Analysis.Asymptotics.Defs` `Mathlib.Analysis.Normed.Field.Basic` `Mathlib.Analysis.Normed.Ring.Basic` `Mathlib.Analysis.Normed.Ring.WithAbs` `Mathlib.LinearAlgebra.Basis.VectorSpace` `Mathlib.RingTheory.MvPolynomial.Ideal` `Mathlib.Topology.MetricSpace.CauSeqFilter`	88
`Mathlib.Algebra.Polynomial.PartialFractions` `Mathlib.Analysis.Normed.Group.AddTorsor`	89
3 files `Mathlib.Algebra.Module.Presentation.DirectSum` `Mathlib.Algebra.Module.Presentation.RestrictScalars` `Mathlib.RingTheory.Finiteness.Subalgebra`	90
`Mathlib.Analysis.Convex.Extrema` `Mathlib.GroupTheory.Coxeter.Basic`	93
`Mathlib.Algebra.Polynomial.OfFn`	94
`Mathlib.Algebra.Module.Projective` `Mathlib.Analysis.Convex.Cone.Closure`	95
5 files `Mathlib.LinearAlgebra.DirectSum.Basis` `Mathlib.LinearAlgebra.Finsupp.VectorSpace` `Mathlib.LinearAlgebra.Matrix.StdBasis` `Mathlib.LinearAlgebra.StdBasis` `Mathlib.LinearAlgebra.TensorProduct.Basis`	96
`Mathlib.Algebra.Order.Module.HahnEmbedding` `Mathlib.LinearAlgebra.Basis.Cardinality`	97
`Mathlib.Algebra.Category.Ring.Adjunctions`	98
5 files `Mathlib.Algebra.Category.AlgCat.Basic` `Mathlib.Algebra.Category.AlgCat.Monoidal` `Mathlib.Algebra.Category.AlgCat.Symmetric` `Mathlib.Algebra.Category.AlgebraCat.Symmetric` `Mathlib.CategoryTheory.Monoidal.Internal.Module`	99
`Mathlib.SetTheory.Surreal.Dyadic`	100
18 files `Mathlib.Algebra.MvPolynomial.Basic` `Mathlib.Algebra.MvPolynomial.Comap` `Mathlib.Algebra.MvPolynomial.CommRing` `Mathlib.Algebra.MvPolynomial.Counit` `Mathlib.Algebra.MvPolynomial.Degrees` `Mathlib.Algebra.MvPolynomial.Division` `Mathlib.Algebra.MvPolynomial.Eval` `Mathlib.Algebra.MvPolynomial.Expand` `Mathlib.Algebra.MvPolynomial.Invertible` `Mathlib.Algebra.MvPolynomial.Monad` `Mathlib.Algebra.MvPolynomial.Rename` `Mathlib.Algebra.MvPolynomial.Supported` `Mathlib.Algebra.MvPolynomial.Variables` `Mathlib.RingTheory.AlgebraicIndependent.Defs` `Mathlib.RingTheory.MvPolynomial.Symmetric.Defs` `Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities` `Mathlib.RingTheory.MvPolynomial.Tower` `Mathlib.Tactic.Ring.NamePolyVars`	101
9 files `Mathlib.Algebra.Category.ModuleCat.Limits` `Mathlib.Algebra.Central.Matrix` `Mathlib.Algebra.FreeAlgebra` `Mathlib.Algebra.Star.Free` `Mathlib.Algebra.Vertex.HVertexOperator` `Mathlib.Algebra.Vertex.VertexOperator` `Mathlib.Data.Matrix.DualNumber` `Mathlib.RingTheory.Adjoin.Basic` `Mathlib.RingTheory.HahnSeries.Multiplication`	102
13 files `Mathlib.Analysis.Convex.Basic` `Mathlib.Analysis.Convex.Cone.Extension` `Mathlib.Analysis.Convex.Extreme` `Mathlib.Analysis.Convex.Function` `Mathlib.Analysis.Convex.Hull` `Mathlib.Analysis.Convex.Join` `Mathlib.Analysis.Convex.Mul` `Mathlib.Analysis.Convex.Piecewise` `Mathlib.Analysis.Convex.Quasiconvex` `Mathlib.Analysis.Convex.Slope` `Mathlib.Geometry.Convex.Cone.Basic` `Mathlib.Geometry.Convex.Cone.Pointed` `Mathlib.LinearAlgebra.TensorPower.Pairing`	103
4 files `Mathlib.Algebra.Module.LocalizedModule.Int` `Mathlib.Algebra.Polynomial.Sequence` `Mathlib.Analysis.Convex.Star` `Mathlib.RingTheory.Localization.NumDen`	104
4 files `Mathlib.Algebra.Category.ModuleCat.Adjunctions` `Mathlib.Algebra.Colimit.Module` `Mathlib.FieldTheory.RatFunc.Defs` `Mathlib.LinearAlgebra.TensorProduct.DirectLimit`	105
`Mathlib.Analysis.Convex.Segment` `Mathlib.RingTheory.Localization.Module`	106
3 files `Mathlib.Algebra.Algebra.Subalgebra.Pi` `Mathlib.Algebra.Category.ModuleCat.Products` `Mathlib.RingTheory.TensorProduct.Pi`	107
21 files `Mathlib.Algebra.Algebra.Operations` `Mathlib.Algebra.Algebra.Subalgebra.Directed` `Mathlib.Algebra.Algebra.Subalgebra.Lattice` `Mathlib.Algebra.Algebra.Subalgebra.MulOpposite` `Mathlib.Algebra.Algebra.Subalgebra.Pointwise` `Mathlib.Algebra.Algebra.Subalgebra.Prod` `Mathlib.Algebra.Algebra.Subalgebra.Tower` `Mathlib.Algebra.Algebra.Subalgebra.Unitization` `Mathlib.Algebra.Central.Basic` `Mathlib.Algebra.Central.Defs` `Mathlib.Algebra.DualNumber` `Mathlib.Algebra.Module.Bimodule` `Mathlib.Algebra.Star.Subalgebra` `Mathlib.Algebra.TrivSqZeroExt` `Mathlib.LinearAlgebra.DirectSum.Finsupp` `Mathlib.LinearAlgebra.DirectSum.TensorProduct` `Mathlib.LinearAlgebra.TensorPower.Basic` `Mathlib.LinearAlgebra.TensorProduct.Opposite` `Mathlib.RingTheory.IsTensorProduct` `Mathlib.RingTheory.PolynomialLaw.Basic` `Mathlib.RingTheory.TensorProduct.Basic`	108
`Mathlib.LinearAlgebra.AffineSpace.Centroid` `Mathlib.LinearAlgebra.AffineSpace.Combination`	109
12 files `Mathlib.Algebra.DirectSum.Algebra` `Mathlib.Algebra.DirectSum.Decomposition` `Mathlib.Algebra.DirectSum.Finsupp` `Mathlib.Algebra.DirectSum.Module` `Mathlib.Algebra.MonoidAlgebra.ToDirectSum` `Mathlib.Combinatorics.Additive.VerySmallDoubling` `Mathlib.Data.Matrix.ColumnRowPartitioned` `Mathlib.LinearAlgebra.DFinsupp` `Mathlib.LinearAlgebra.LinearIndependent.Lemmas` `Mathlib.LinearAlgebra.Multilinear.DFinsupp` `Mathlib.LinearAlgebra.SesquilinearForm` `Mathlib.RingTheory.Ideal.Basis`	110
5 files `Mathlib.Algebra.Polynomial.HasseDeriv` `Mathlib.LinearAlgebra.Alternating.Basic` `Mathlib.LinearAlgebra.Alternating.Curry` `Mathlib.LinearAlgebra.Basis.Exact` `Mathlib.LinearAlgebra.Ray`	111
`Mathlib.Algebra.Polynomial.DenomsClearable`	112
`Mathlib.Algebra.Polynomial.Cardinal`	113
4 files `Mathlib.Data.Nat.Choose.Cast` `Mathlib.Data.Nat.Factorial.Cast` `Mathlib.NumberTheory.Multiplicity` `Mathlib.RingTheory.Polynomial.Pochhammer`	114
4 files `Mathlib.Algebra.Polynomial.Eval.Subring` `Mathlib.RingTheory.IntegralClosure.Algebra.Defs` `Mathlib.RingTheory.IntegralClosure.IsIntegral.Defs` `Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Defs`	119
`Mathlib.Algebra.Polynomial.Div` `Mathlib.Algebra.Polynomial.UnitTrinomial`	121
`Mathlib.Data.Finsupp.MonomialOrder.DegLex` `Mathlib.SetTheory.Surreal.Multiplication`	122
8 files `Mathlib.Algebra.Module.Presentation.Basic` `Mathlib.Algebra.Module.Presentation.Cokernel` `Mathlib.Algebra.Module.Presentation.Tautological` `Mathlib.Algebra.Module.Presentation.Tensor` `Mathlib.Algebra.Polynomial.BigOperators` `Mathlib.Algebra.Polynomial.Mirror` `Mathlib.Algebra.Polynomial.Monic` `Mathlib.Algebra.Polynomial.Reverse`	124
3 files `Mathlib.Analysis.Normed.Group.Submodule` `Mathlib.Combinatorics.SimpleGraph.Triangle.Counting` `Mathlib.Computability.TMComputable`	125
`Mathlib.Algebra.SkewMonoidAlgebra.Support` `Mathlib.RingTheory.Ideal.Basic`	126
10 files `Mathlib.Algebra.Group.ForwardDiff` `Mathlib.Algebra.Polynomial.CancelLeads` `Mathlib.Algebra.Polynomial.CoeffList` `Mathlib.Algebra.Polynomial.Degree.Lemmas` `Mathlib.Algebra.Polynomial.Degree.TrailingDegree` `Mathlib.Algebra.Polynomial.EraseLead` `Mathlib.Algebra.Polynomial.Eval.Degree` `Mathlib.Algebra.Polynomial.Eval.Irreducible` `Mathlib.Algebra.Polynomial.Inductions` `Mathlib.Tactic.ComputeDegree`	127
`Mathlib.Algebra.SkewMonoidAlgebra.Basic` `Mathlib.LinearAlgebra.Basis.Prod`	129
20 files `Mathlib.Algebra.Polynomial.Degree.Domain` `Mathlib.Algebra.Polynomial.Degree.Operations` `Mathlib.Algebra.Polynomial.Degree.SmallDegree` `Mathlib.Algebra.Polynomial.Degree.Support` `Mathlib.Algebra.Polynomial.Degree.Units` `Mathlib.Algebra.Polynomial.Derivative` `Mathlib.Algebra.Polynomial.Eval.SMul` `Mathlib.Algebra.Polynomial.Identities` `Mathlib.Combinatorics.Optimization.ValuedCSP` `Mathlib.Data.Matrix.Auto` `Mathlib.Data.Matrix.Reflection` `Mathlib.GroupTheory.Coxeter.Matrix` `Mathlib.LinearAlgebra.BilinearForm.Hom` `Mathlib.LinearAlgebra.Matrix.Circulant` `Mathlib.LinearAlgebra.Matrix.DotProduct` `Mathlib.LinearAlgebra.Matrix.Hadamard` `Mathlib.LinearAlgebra.Matrix.Notation` `Mathlib.LinearAlgebra.Matrix.Trace` `Mathlib.RingTheory.Polynomial.Hermite.Basic` `Mathlib.RingTheory.Polynomial.Opposites`	130
11 files `Mathlib.Algebra.Order.Antidiag.Nat` `Mathlib.Analysis.Normed.Group.Subgroup` `Mathlib.Data.Matrix.Block` `Mathlib.Data.Matrix.Invertible` `Mathlib.LinearAlgebra.Basis.Fin` `Mathlib.LinearAlgebra.Basis.Submodule` `Mathlib.LinearAlgebra.Matrix.ConjTranspose` `Mathlib.LinearAlgebra.Matrix.Permanent` `Mathlib.LinearAlgebra.Matrix.RowCol` `Mathlib.LinearAlgebra.Matrix.Symmetric` `Mathlib.RingTheory.AlgebraTower`	131
6 files `Mathlib.Combinatorics.SimpleGraph.Triangle.Basic` `Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite` `Mathlib.LinearAlgebra.Multilinear.Basis` `Mathlib.Topology.Metrizable.CompletelyMetrizable` `Mathlib.Topology.Metrizable.ContinuousMap` `Mathlib.Topology.Metrizable.Uniformity`	132
6 files `Mathlib.Algebra.Polynomial.Coeff` `Mathlib.Algebra.Polynomial.Eval.Coeff` `Mathlib.Analysis.Normed.Group.Constructions` `Mathlib.Analysis.Normed.Group.Int` `Mathlib.Analysis.NormedSpace.MStructure` `Mathlib.Data.Nat.Choose.Vandermonde`	133
13 files `Mathlib.Algebra.Module.Submodule.Pointwise` `Mathlib.Analysis.BoxIntegral.Box.Basic` `Mathlib.Analysis.BoxIntegral.Partition.Basic` `Mathlib.Analysis.BoxIntegral.Partition.Split` `Mathlib.Analysis.BoxIntegral.Partition.Tagged` `Mathlib.Analysis.Normed.Group.Basic` `Mathlib.Analysis.Normed.Group.CocompactMap` `Mathlib.Analysis.Normed.Group.Indicator` `Mathlib.Analysis.Normed.Order.Basic` `Mathlib.Analysis.Normed.Order.Hom.Basic` `Mathlib.Analysis.Normed.Order.Hom.Ultra` `Mathlib.Analysis.NormedSpace.IndicatorFunction` `Mathlib.InformationTheory.Hamming`	134
4 files `Mathlib.Algebra.Algebra.Subalgebra.Matrix` `Mathlib.Data.Matrix.Bilinear` `Mathlib.NumberTheory.Basic` `Mathlib.NumberTheory.SelbergSieve`	135
`Mathlib.NumberTheory.ArithmeticFunction`	136
4 files `Mathlib.Data.Matrix.Basic` `Mathlib.Data.Matrix.Basis` `Mathlib.Data.Matrix.Composition` `Mathlib.LinearAlgebra.Matrix.Unique`	137
`Mathlib.LinearAlgebra.Basis.Flag`	138
3 files `Mathlib.Data.Finsupp.MonomialOrder` `Mathlib.Data.Finsupp.WellFounded` `Mathlib.LinearAlgebra.FreeModule.Basic`	141
`Mathlib.Algebra.CharP.Reduced` `Mathlib.NumberTheory.MaricaSchoenheim`	143
`Mathlib.LinearAlgebra.Finsupp.Pi`	144
`Mathlib.LinearAlgebra.Basis.Basic` `Mathlib.LinearAlgebra.Basis.SMul`	145
`Mathlib.Data.Nat.Squarefree` `Mathlib.NumberTheory.SmoothNumbers`	146
`Mathlib.Algebra.CharP.Frobenius` `Mathlib.Algebra.MonoidAlgebra.Ideal`	147
`Mathlib.RingTheory.Radical`	151
`Mathlib.NumberTheory.Padics.PadicNorm`	153
`Mathlib.NumberTheory.Padics.PadicVal.Basic` `Mathlib.SetTheory.Cardinal.Finsupp`	155
`Mathlib.Algebra.CharP.Lemmas` `Mathlib.CategoryTheory.Action.Monoidal`	157
`Mathlib.Data.Nat.Choose.Factorization` `Mathlib.Data.Nat.Multiplicity`	158
`Mathlib.Algebra.Squarefree.Basic` `Mathlib.RingTheory.HahnSeries.Lex`	159
`Mathlib.Algebra.Polynomial.Degree.Definitions` `Mathlib.Algebra.Polynomial.Degree.Monomial`	161
`Mathlib.Data.Nat.Factorization.PrimePow`	164
`Mathlib.SetTheory.Ordinal.CantorNormalForm`	165
`Mathlib.LinearAlgebra.LinearIndependent.Basic`	168
`Mathlib.Data.ENNReal.BigOperators`	169
3 files `Mathlib.Algebra.Homology.AlternatingConst` `Mathlib.Data.Nat.Factorization.Basic` `Mathlib.Data.Nat.Factorization.LCM`	170
`Mathlib.Data.NNReal.Basic`	172
`Mathlib.Data.Complex.BigOperators`	175
`Mathlib.RingTheory.Nilpotent.Basic`	176
18 files `Mathlib.Algebra.Order.BigOperators.Expect` `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.HomotopyEquivalence` `Mathlib.AlgebraicTopology.DoldKan.NCompGamma` `Mathlib.AlgebraicTopology.DoldKan.NReflectsIso` `Mathlib.AlgebraicTopology.DoldKan.Normalized` `Mathlib.AlgebraicTopology.DoldKan.PInfty` `Mathlib.AlgebraicTopology.DoldKan.Projections` `Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject` `Mathlib.Logic.Hydra`	177
5 files `Mathlib.Algebra.FreeNonUnitalNonAssocAlgebra` `Mathlib.Algebra.MonoidAlgebra.Basic` `Mathlib.Combinatorics.Enumerative.Bell` `Mathlib.Data.Nat.Choose.Multinomial` `Mathlib.LinearAlgebra.Finsupp.Span`	178
5 files `Mathlib.AlgebraicTopology.DoldKan.Homotopies` `Mathlib.AlgebraicTopology.ExtraDegeneracy` `Mathlib.Data.Nat.Factorization.Defs` `Mathlib.Data.Nat.Factorization.Induction` `Mathlib.Data.Nat.Factorization.Root`	180
3 files `Mathlib.AlgebraicTopology.AlternatingFaceMapComplex` `Mathlib.AlgebraicTopology.DoldKan.Notations` `Mathlib.LinearAlgebra.SModEq`	181
`Mathlib.LinearAlgebra.Countable`	182
`Mathlib.Algebra.BigOperators.Balance` `Mathlib.Algebra.BigOperators.Expect`	183
`Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform`	186
4 files `Mathlib.Algebra.MonoidAlgebra.Degree` `Mathlib.Algebra.Polynomial.Basis` `Mathlib.Data.Finsupp.Lex` `Mathlib.LinearAlgebra.Dual.Basis`	187
`Mathlib.Algebra.MonoidAlgebra.Support` `Mathlib.NumberTheory.Primorial`	188
3 files `Mathlib.Data.Finsupp.Weight` `Mathlib.LinearAlgebra.Basis.Bilinear` `Mathlib.LinearAlgebra.Basis.Defs`	192
`Mathlib.LinearAlgebra.Matrix.SemiringInverse`	194
`Mathlib.NumberTheory.FactorisationProperties`	195
5 files `Mathlib.Algebra.Polynomial.Basic` `Mathlib.Algebra.Polynomial.Eval.Algebra` `Mathlib.Algebra.Polynomial.Eval.Defs` `Mathlib.Algebra.Polynomial.Monomial` `Mathlib.Combinatorics.SetFamily.AhlswedeZhang`	196
`Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid`	198
`Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet`	199
`Mathlib.Combinatorics.Enumerative.Catalan` `Mathlib.Combinatorics.Enumerative.DyckWord`	200
`Mathlib.RingTheory.UniqueFactorizationDomain.Finsupp`	201
5 files `Mathlib.Algebra.Category.ModuleCat.Colimits` `Mathlib.Algebra.Category.ModuleCat.FilteredColimits` `Mathlib.Algebra.MonoidAlgebra.Module` `Mathlib.Combinatorics.Enumerative.IncidenceAlgebra` `Mathlib.RingTheory.HahnSeries.Addition`	202
`Mathlib.Algebra.Order.CauSeq.BigOperators`	203
`Mathlib.LinearAlgebra.LinearIndependent.Defs`	206
`Mathlib.Algebra.Ring.Divisibility.Lemmas`	207
3 files `Mathlib.Data.Finsupp.Interval` `Mathlib.LinearAlgebra.Finsupp.LinearCombination` `Mathlib.LinearAlgebra.Finsupp.Supported`	208
`Mathlib.Combinatorics.SetFamily.LYM`	209
`Mathlib.Algebra.Category.Grp.Colimits`	210
`Mathlib.Combinatorics.Additive.SmallTripling` `Mathlib.Combinatorics.Derangements.Finite`	212
`Mathlib.Algebra.Order.Ring.IsNonarchimedean` `Mathlib.Data.Nat.Choose.Sum`	216
`Mathlib.LinearAlgebra.Finsupp.LSum`	218
`Mathlib.RingTheory.UniqueFactorizationDomain.Nat`	219
`Mathlib.Algebra.GeomSum` `Mathlib.RingTheory.ChainOfDivisors`	220
3 files `Mathlib.Algebra.Order.Antidiag.Finsupp` `Mathlib.Combinatorics.SetFamily.KruskalKatona` `Mathlib.LinearAlgebra.Matrix.Integer`	221
`Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity`	224
6 files `Mathlib.Algebra.GroupWithZero.Torsion` `Mathlib.Combinatorics.Additive.DoublingConst` `Mathlib.Combinatorics.Additive.PluenneckeRuzsa` `Mathlib.RingTheory.UniqueFactorizationDomain.Finite` `Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative` `Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors`	225
`Mathlib.RingTheory.UniqueFactorizationDomain.Basic`	226
`Mathlib.Algebra.DirectSum.AddChar`	233
`Mathlib.Combinatorics.Additive.Energy` `Mathlib.Data.Finsupp.Encodable`	235
`Mathlib.Algebra.FreeAbelianGroup.UniqueSums` `Mathlib.CategoryTheory.Preadditive.Mat`	239
`Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors` `Mathlib.Combinatorics.Colex`	240
`Mathlib.Topology.Algebra.Monoid.AddChar`	241
`Mathlib.Combinatorics.SimpleGraph.IncMatrix`	242
3 files `Mathlib.Combinatorics.Enumerative.Composition` `Mathlib.Combinatorics.Enumerative.Partition` `Mathlib.Data.Matrix.Action`	244
4 files `Mathlib.Combinatorics.Additive.AP.Three.Defs` `Mathlib.Data.Matrix.Mul` `Mathlib.Data.Matrix.PEquiv` `Mathlib.LinearAlgebra.Matrix.Orthogonal`	245
`Mathlib.Combinatorics.Enumerative.InclusionExclusion` `Mathlib.Tactic.NormNum.IsCoprime`	246
4 files `Mathlib.Algebra.Order.BigOperators.Ring.Finset` `Mathlib.Data.Finsupp.Order` `Mathlib.Data.NNRat.BigOperators` `Mathlib.Data.Nat.Factorial.BigOperators`	248
`Mathlib.Algebra.Order.Ring.GeomSum`	249
`Mathlib.Testing.Plausible.Functions`	251
`Mathlib.Algebra.BigOperators.Field` `Mathlib.Algebra.FreeAbelianGroup.Finsupp`	252
`Mathlib.Data.DFinsupp.Small` `Mathlib.Data.Finsupp.Antidiagonal`	253
`Mathlib.Algebra.MonoidAlgebra.Opposite` `Mathlib.LinearAlgebra.Finsupp.SumProd`	254
9 files `Mathlib.Algebra.BigOperators.Finsupp.Fin` `Mathlib.Algebra.MonoidAlgebra.Defs` `Mathlib.Algebra.MonoidAlgebra.Division` `Mathlib.Algebra.MonoidAlgebra.Lift` `Mathlib.Algebra.MonoidAlgebra.MapDomain` `Mathlib.Algebra.Order.Antidiag.Pi` `Mathlib.Data.Finsupp.SMul` `Mathlib.Data.Finsupp.ToDFinsupp` `Mathlib.LinearAlgebra.Finsupp.Defs`	255
`Mathlib.Data.Finsupp.Multiset`	260
`Mathlib.Algebra.Order.Field.GeomSum`	261
`Mathlib.RingTheory.Coprime.Lemmas`	263
`Mathlib.Data.Fin.Tuple.NatAntidiagonal`	264
`Mathlib.Algebra.Category.MonCat.Adjunctions`	265
`Mathlib.Algebra.BigOperators.Fin` `Mathlib.Data.Fin.Tuple.Reflection`	267
`Mathlib.Data.Finsupp.Option`	269
`Mathlib.Data.Finset.Finsupp`	271
3 files `Mathlib.Algebra.Field.GeomSum` `Mathlib.Combinatorics.Enumerative.DoubleCounting` `Mathlib.Data.Finsupp.AList`	272
`Mathlib.Data.Finsupp.Basic`	273
`Mathlib.Algebra.Ring.GeomSum`	274
3 files `Mathlib.Combinatorics.Additive.Corner.Defs` `Mathlib.Combinatorics.Additive.FreimanHom` `Mathlib.MeasureTheory.Constructions.AddChar`	280
`Mathlib.Algebra.BigOperators.Associated`	288
`Mathlib.Algebra.Group.Subgroup.Finsupp`	296
`Mathlib.Algebra.BigOperators.Finsupp.Basic` `Mathlib.Algebra.Group.Submonoid.Finsupp`	300
`Mathlib.Algebra.Group.AddChar`	301
`Mathlib.Algebra.BigOperators.Ring.Finset`	322

Declarations diff

+ sum_negOnePow_smul_add_consecutive
+ sum_negOnePow_smul_add_consecutive_succ

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).

Mathlib/Algebra/BigOperators/Intervals.lean

Address reviewer feedback from PR leanprover-community#29643: - Generalize theorem from integers to any Ring R - Remove redundant sum_range_succ_eq_head lemma - Simplify statement by directly using (a k + b k) - Rename variables: b→a, c→b for consistency - All simps are already squeezed (using simp only) 🤖 Generated with [Claude Code](https://claude.ai/code) Co-Authored-By: Claude <noreply@anthropic.com>

Mathlib/Algebra/BigOperators/Intervals.lean

@plp127

- Simplify theorem to use only one sequence a (removed parameter b) - Use direct power notation (-1)^k instead of Int.negOnePow - Merge proof steps and remove unnecessary section - Maintain Ring R requirement for multiplication Thanks to @plp127 for the helpful suggestions! Addresses all feedback from @plp127 on PR leanprover-community#29643

jessealama · 2025-09-14T19:01:09Z

I believe I've addressed your feedback. The proof is unfortunately a bit bulkier. Can you please take another look?

Mathlib/Algebra/BigOperators/Intervals.lean

- Generalize to Module over Ring instead of AddCommGroup over ℤ - Move theorems out of Finset namespace into new TelescopingSum section - Keep Int.negOnePow as suggested Based on reviewer feedback on PR leanprover-community#29643

jessealama · 2025-09-15T08:24:38Z

In the build logs, I see that adding the Mathlib.Algebra.Ring.NegOnePow in Mathlib.Algebra.BigOperators.Intervals triggers violations on some bans about what can be imported where. We could either go back to the "plain" version that uses -1 and/or try to find a better place for this result. Perhaps Mathlib.Algebra.BigOperators.Ring.Finset?

Add two theorems for alternating telescoping sums that reduce to boundary terms. These are useful for computing Euler characteristics in chain complexes. - sum_negOnePow_smul_add_consecutive_succ: inclusive version (0 to n) - sum_negOnePow_smul_add_consecutive: standard version (0 to n-1) 🤖 Generated with [Claude Code](https://claude.ai/code) Co-Authored-By: Claude <noreply@anthropic.com>

jessealama · 2025-09-15T12:18:56Z

In the build logs, I see that adding the Mathlib.Algebra.Ring.NegOnePow in Mathlib.Algebra.BigOperators.Intervals triggers violations on some bans about what can be imported where. We could either go back to the "plain" version that uses (-1 : Z) and/or try to find a better place for this result. Perhaps Mathlib.Algebra.BigOperators.Ring.Finset?

Adding the theorem to Mathlib.Algebra.BigOperators.Ring.Finset also causes problems with the build. Shall we put this in its own new module? Alternatively, we could just restate in terms of -1.

@joelriou

This PR contributes the Euler-Poincaré formula for bounded chain complexes of finite-dimensional vector spaces over a field. ## Main Contributions ### Core Theorem * `ChainComplex.euler_poincare_formula`: The Euler-Poincaré formula showing that the alternating sum of chain space dimensions equals the alternating sum of homology dimensions for bounded complexes ### Supporting Infrastructure * Euler characteristic definitions in `EulerCharacteristic.lean`: - `ChainComplex.boundedEulerChar`: Bounded Euler characteristic - `ChainComplex.homologyBoundedEulerChar`: Homological Euler characteristic * General chain complex lemmas added to `HomologicalComplex.lean` * Private telescoping sum lemma for the main proof ## Related Work This is part of a multi-PR contribution towards formalizing Euler's polyhedron formula (Wiedijk leanprover-community#13). Related to: - PR leanprover-community#29643 (telescoping sum infrastructure) - PR leanprover-community#29639 (original combined PR) ## Acknowledgments Thanks to @joelriou for valuable feedback on the original PR. 🤖 Generated with [Claude Code](https://claude.ai/code) Co-Authored-By: Claude <noreply@anthropic.com>

jessealama · 2025-09-18T08:25:42Z

The telescoping sum work has been reworked in #29713 to apply to sums over integer indexes rather than natural number indices starting from 0. This work seems valid to me but I'm inclined to close this PR. I notice we have Finset.sum_range_tsub in Mathlib.Algebra.BigOperators.Group.Finset.Basic, which is largely the same as what we're trying to do in this branch.

github-actions bot added new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-algebra Algebra (groups, rings, fields, etc) labels Sep 14, 2025

plp127 reviewed Sep 14, 2025

View reviewed changes

Mathlib/Algebra/BigOperators/Intervals.lean Outdated Show resolved Hide resolved

plp127 reviewed Sep 14, 2025

View reviewed changes

Mathlib/Algebra/BigOperators/Intervals.lean Outdated Show resolved Hide resolved

plp127 reviewed Sep 14, 2025

View reviewed changes

Mathlib/Algebra/BigOperators/Intervals.lean Outdated Show resolved Hide resolved

plp127 reviewed Sep 14, 2025

View reviewed changes

Mathlib/Algebra/BigOperators/Intervals.lean Outdated Show resolved Hide resolved

plp127 reviewed Sep 14, 2025

View reviewed changes

Mathlib/Algebra/BigOperators/Intervals.lean Outdated Show resolved Hide resolved

jessealama force-pushed the telescoping-sum branch from 4d4aae7 to 3fe90c9 Compare September 14, 2025 17:41

jessealama requested a review from plp127 September 14, 2025 17:42

plp127 requested changes Sep 14, 2025

View reviewed changes

jessealama mentioned this pull request Sep 14, 2025

feat: Euler's polyhedron formula via homological algebra #29639

Closed

github-actions bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label Sep 14, 2025

jessealama force-pushed the telescoping-sum branch from d4c25be to 8b2ce1d Compare September 14, 2025 19:22

jessealama requested a review from plp127 September 14, 2025 19:23

plp127 reviewed Sep 14, 2025

View reviewed changes

Mathlib/Algebra/BigOperators/Intervals.lean Outdated Show resolved Hide resolved

plp127 reviewed Sep 14, 2025

View reviewed changes

Mathlib/Algebra/BigOperators/Intervals.lean Outdated Show resolved Hide resolved

plp127 reviewed Sep 14, 2025

View reviewed changes

Mathlib/Algebra/BigOperators/Intervals.lean Outdated Show resolved Hide resolved

jessealama force-pushed the telescoping-sum branch 3 times, most recently from 1f56e41 to 8c82c23 Compare September 14, 2025 21:48

jessealama requested a review from plp127 September 14, 2025 21:49

plp127 reviewed Sep 14, 2025

View reviewed changes

Mathlib/Algebra/BigOperators/Intervals.lean Outdated Show resolved Hide resolved

jessealama force-pushed the telescoping-sum branch from 8c82c23 to 465026e Compare September 14, 2025 22:14

plp127 reviewed Sep 14, 2025

View reviewed changes

Mathlib/Algebra/BigOperators/Intervals.lean Outdated Show resolved Hide resolved

jessealama force-pushed the telescoping-sum branch from 465026e to 2e1a7d4 Compare September 14, 2025 22:19

jessealama requested a review from plp127 September 14, 2025 22:20

plp127 reviewed Sep 14, 2025

View reviewed changes

Mathlib/Algebra/BigOperators/Intervals.lean Outdated Show resolved Hide resolved

jessealama force-pushed the telescoping-sum branch 2 times, most recently from 3ed9c5d to 39ac716 Compare September 15, 2025 07:58

jessealama requested a review from plp127 September 15, 2025 08:00

jessealama force-pushed the telescoping-sum branch from 39ac716 to 3a348ef Compare September 15, 2025 08:06

jessealama force-pushed the telescoping-sum branch from 18a98cb to 29f3eba Compare September 15, 2025 12:12

jessealama mentioned this pull request Sep 16, 2025

feat(Algebra/Homology): add Euler–Poincaré formula #29713

Draft

jessealama closed this Sep 18, 2025

Conversation

jessealama commented Sep 14, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

Theorems Added

Details

Context

Uh oh!

github-actions bot commented Sep 14, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 82ba83d8bc

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

jessealama commented Sep 14, 2025

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

jessealama commented Sep 15, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

jessealama commented Sep 15, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

jessealama commented Sep 18, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

jessealama commented Sep 14, 2025 •

edited

Loading

github-actions bot commented Sep 14, 2025 •

edited

Loading

jessealama commented Sep 15, 2025 •

edited

Loading

jessealama commented Sep 15, 2025 •

edited

Loading