Skip to content

feat(NumberTheory/Height/Basic): add bounds for sums #34330

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Open
MichaelStollBayreuth wants to merge 6 commits into
base: master
Choose a base branch
from
Open

feat(NumberTheory/Height/Basic): add bounds for sums #34330

MichaelStollBayreuth wants to merge 6 commits into from
+284 −12

Conversation

@MichaelStollBayreuth
Copy link
Collaborator

@MichaelStollBayreuth MichaelStollBayreuth commented Jan 23, 2026 •
edited
Loading

The main purpose of this PR (no. 3 in the series on heights) is to state and prove bounds for the height of x + y and for the height of a finite sum of field elements.

In addition, we add positivity extensions for multiplicative and logarithmic heights (this is cargo-culted code, but it seemst to be working); this simplifies some of the proofs, in particular in the context of pulling log outwards.

Finally, we fill some holes in the API for products on Multisets and for finprods.

Open in Gitpod

@MichaelStollBayreuth MichaelStollBayreuth added awaiting-CI This PR doesn't pass CI yet. This label is automatically removed once it does. t-number-theory Number theory (also use t-algebra or t-analysis to specialize) labels Jan 23, 2026
@github-actions github-actions bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label Jan 23, 2026
@github-actions
Copy link

github-actions bot commented Jan 23, 2026

PR summary c99f041082

Import changes exceeding 2%

% File
+15.26% Mathlib.Algebra.BigOperators.Finprod

Import changes for modified files

Dependency changes

File Base Count Head Count Change
Mathlib.Algebra.BigOperators.Finprod 603 695 +92 (+15.26%)
Mathlib.NumberTheory.Height.Basic 1672 1674 +2 (+0.12%)
Import changes for all files
Files Import difference
Mathlib.NumberTheory.Height.Instances 1
Mathlib.NumberTheory.Height.Basic 2
163 files Mathlib.Algebra.Category.ContinuousCohomology.Basic Mathlib.Algebra.Category.ModuleCat.Topology.Basic Mathlib.Algebra.Category.ModuleCat.Topology.Homology Mathlib.Algebra.Category.Ring.Topology Mathlib.Algebra.Polynomial.Degree.CardPowDegree Mathlib.AlgebraicGeometry.AffineScheme Mathlib.AlgebraicGeometry.Cover.Directed Mathlib.AlgebraicGeometry.Cover.Over Mathlib.AlgebraicGeometry.Cover.QuasiCompact Mathlib.AlgebraicGeometry.Cover.Sigma Mathlib.AlgebraicGeometry.Fiber Mathlib.AlgebraicGeometry.FunctionField Mathlib.AlgebraicGeometry.GluingOneHypercover Mathlib.AlgebraicGeometry.IdealSheaf.Basic Mathlib.AlgebraicGeometry.IdealSheaf.Functorial Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme Mathlib.AlgebraicGeometry.LimitsOver 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.Finite Mathlib.AlgebraicGeometry.Morphisms.Flat Mathlib.AlgebraicGeometry.Morphisms.Immersion Mathlib.AlgebraicGeometry.Morphisms.Integral Mathlib.AlgebraicGeometry.Morphisms.IsIso Mathlib.AlgebraicGeometry.Morphisms.LocalClosure Mathlib.AlgebraicGeometry.Morphisms.LocalIso Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion Mathlib.AlgebraicGeometry.Morphisms.Preimmersion Mathlib.AlgebraicGeometry.Morphisms.Proper Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties Mathlib.AlgebraicGeometry.Morphisms.Separated Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective Mathlib.AlgebraicGeometry.Noetherian Mathlib.AlgebraicGeometry.Normalization Mathlib.AlgebraicGeometry.PointsPi Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic Mathlib.AlgebraicGeometry.Properties Mathlib.AlgebraicGeometry.PullbackCarrier Mathlib.AlgebraicGeometry.Pullbacks Mathlib.AlgebraicGeometry.QuasiAffine Mathlib.AlgebraicGeometry.RationalMap Mathlib.AlgebraicGeometry.RelativeGluing Mathlib.AlgebraicGeometry.ResidueField Mathlib.AlgebraicGeometry.Sites.BigZariski Mathlib.AlgebraicGeometry.Sites.Pretopology Mathlib.AlgebraicGeometry.Sites.Representability Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski Mathlib.AlgebraicGeometry.Sites.Small Mathlib.AlgebraicGeometry.SpreadingOut Mathlib.AlgebraicGeometry.Stalk Mathlib.AlgebraicGeometry.ValuativeCriterion 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.Analysis.CStarAlgebra.Module.Synonym Mathlib.Analysis.Complex.IsIntegral Mathlib.Analysis.Convex.Cone.Basic Mathlib.Analysis.Convex.Cone.Extension Mathlib.Analysis.Convex.ContinuousLinearEquiv Mathlib.Analysis.Convex.Contractible Mathlib.Analysis.Convex.Exposed Mathlib.Analysis.Convex.Extrema Mathlib.Analysis.Convex.PathConnected Mathlib.Analysis.Convex.Quasiconvex Mathlib.Analysis.Fourier.Notation Mathlib.Combinatorics.Enumerative.Partition.GenFun Mathlib.Combinatorics.Enumerative.Partition.Glaisher Mathlib.Data.Complex.BigOperators Mathlib.LinearAlgebra.Complex.Module Mathlib.LinearAlgebra.Projectivization.Constructions Mathlib.NumberTheory.Zsqrtd.GaussianInt Mathlib.RingTheory.AdicCompletion.Topology Mathlib.RingTheory.MvPowerSeries.Evaluation Mathlib.RingTheory.MvPowerSeries.Expand Mathlib.RingTheory.MvPowerSeries.LinearTopology Mathlib.RingTheory.MvPowerSeries.PiTopology Mathlib.RingTheory.MvPowerSeries.Substitution Mathlib.RingTheory.Polynomial.GaussNorm Mathlib.RingTheory.PowerSeries.Evaluation Mathlib.RingTheory.PowerSeries.Expand Mathlib.RingTheory.PowerSeries.GaussNorm Mathlib.RingTheory.PowerSeries.PiTopology Mathlib.RingTheory.PowerSeries.Substitution Mathlib.RingTheory.Valuation.ValuativeRel.Basic Mathlib.RingTheory.Valuation.ValuativeRel.Trivial Mathlib.RingTheory.Valuation.ValuativeRel Mathlib.Topology.Algebra.AffineSubspace Mathlib.Topology.Algebra.Algebra.Equiv Mathlib.Topology.Algebra.Algebra Mathlib.Topology.Algebra.ContinuousAffineEquiv Mathlib.Topology.Algebra.ContinuousAffineMap Mathlib.Topology.Algebra.FilterBasis Mathlib.Topology.Algebra.Group.CompactOpen Mathlib.Topology.Algebra.InfiniteSum.Module Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean Mathlib.Topology.Algebra.InfiniteSum.Ring Mathlib.Topology.Algebra.IntermediateField Mathlib.Topology.Algebra.IsOpenUnits Mathlib.Topology.Algebra.LinearMapCompletion Mathlib.Topology.Algebra.Module.Alternating.Basic Mathlib.Topology.Algebra.Module.Basic Mathlib.Topology.Algebra.Module.CharacterSpace Mathlib.Topology.Algebra.Module.ClosedSubmodule Mathlib.Topology.Algebra.Module.Compact Mathlib.Topology.Algebra.Module.Equiv Mathlib.Topology.Algebra.Module.LinearMapPiProd Mathlib.Topology.Algebra.Module.LinearMap Mathlib.Topology.Algebra.Module.LinearPMap Mathlib.Topology.Algebra.Module.ModuleTopology Mathlib.Topology.Algebra.Module.Multilinear.Basic Mathlib.Topology.Algebra.Module.PerfectPairing Mathlib.Topology.Algebra.Module.Simple Mathlib.Topology.Algebra.Module.Star Mathlib.Topology.Algebra.Module.WeakBilin Mathlib.Topology.Algebra.Module.WeakDual Mathlib.Topology.Algebra.MvPolynomial Mathlib.Topology.Algebra.NonUnitalAlgebra Mathlib.Topology.Algebra.NonUnitalStarAlgebra Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology Mathlib.Topology.Algebra.Nonarchimedean.Bases Mathlib.Topology.Algebra.SeparationQuotient.Basic Mathlib.Topology.Algebra.SeparationQuotient.FiniteDimensional Mathlib.Topology.Algebra.SeparationQuotient.Hom Mathlib.Topology.Algebra.SeparationQuotient.Section Mathlib.Topology.Algebra.StarSubalgebra Mathlib.Topology.Algebra.TopologicallyNilpotent Mathlib.Topology.Algebra.UniformFilterBasis Mathlib.Topology.Algebra.Valued.ValuationTopology Mathlib.Topology.Algebra.Valued.ValuativeRel Mathlib.Topology.Algebra.Valued.ValuedField Mathlib.Topology.ContinuousMap.Algebra Mathlib.Topology.ContinuousMap.Lattice Mathlib.Topology.ContinuousMap.LocallyConstant Mathlib.Topology.ContinuousMap.Periodic Mathlib.Topology.ContinuousMap.Star Mathlib.Topology.Homotopy.Affine Mathlib.Topology.Homotopy.Contractible Mathlib.Topology.Homotopy.HomotopyGroup Mathlib.Topology.Homotopy.Lifting Mathlib.Topology.Homotopy.LocallyContractible Mathlib.Topology.Homotopy.Path Mathlib.Topology.Homotopy.Product Mathlib.Topology.Instances.RealVectorSpace Mathlib.Topology.Instances.TrivSqZeroExt Mathlib.Topology.MetricSpace.Algebra Mathlib.Topology.MetricSpace.Completion Mathlib.Topology.Sheaves.CommRingCat Mathlib.Topology.Subpath Mathlib.Topology.UniformSpace.ProdApproximation
 6
296 files Mathlib.Algebra.BrauerGroup.Defs Mathlib.Algebra.Category.CommAlgCat.Basic Mathlib.Algebra.Category.CommAlgCat.FiniteType Mathlib.Algebra.Category.CommAlgCat.Monoidal Mathlib.Algebra.Category.CommBialgCat 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.Descent Mathlib.Algebra.Category.ModuleCat.Ext.HasExt Mathlib.Algebra.Category.Ring.Constructions Mathlib.Algebra.Category.Ring.Instances Mathlib.Algebra.Category.Ring.LinearAlgebra Mathlib.Algebra.Category.Ring.Under.Basic Mathlib.Algebra.Category.Ring.Under.Limits Mathlib.Algebra.CharP.CharAndCard Mathlib.Algebra.CharP.Quotient Mathlib.Algebra.DirectSum.LinearMap Mathlib.Algebra.GCDMonoid.IntegrallyClosed Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences Mathlib.Algebra.Homology.DerivedCategory.KInjective Mathlib.Algebra.Homology.DerivedCategory.KProjective Mathlib.Algebra.Homology.DerivedCategory.SmallShiftedHom Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle Mathlib.Algebra.Lie.CartanMatrix Mathlib.Algebra.Lie.CartanSubalgebra Mathlib.Algebra.Lie.EngelSubalgebra Mathlib.Algebra.Lie.Engel Mathlib.Algebra.Lie.InvariantForm Mathlib.Algebra.Lie.Nilpotent Mathlib.Algebra.Lie.SerreConstruction Mathlib.Algebra.Module.Submodule.Union Mathlib.Algebra.Order.Module.HahnEmbedding Mathlib.Algebra.Order.Ring.Archimedean Mathlib.Algebra.Polynomial.Bivariate Mathlib.Algebra.Polynomial.DenomsClearable Mathlib.Algebra.Polynomial.UnitTrinomial Mathlib.AlgebraicGeometry.Cover.MorphismProperty Mathlib.AlgebraicGeometry.Cover.Open Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula 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.ProjectiveSpectrum.StructureSheaf Mathlib.AlgebraicGeometry.Restrict Mathlib.AlgebraicGeometry.Scheme Mathlib.AlgebraicGeometry.Sites.MorphismProperty Mathlib.AlgebraicGeometry.Spec Mathlib.AlgebraicGeometry.StructureSheaf Mathlib.Analysis.Convex.BetweenList Mathlib.Analysis.Convex.Between Mathlib.Analysis.Convex.Function Mathlib.Analysis.Convex.Mul Mathlib.Analysis.Convex.Piecewise Mathlib.Analysis.Convex.Slope Mathlib.Analysis.Convex.Strict Mathlib.CategoryTheory.Abelian.GrothendieckCategory.HasExt Mathlib.CategoryTheory.Abelian.Injective.Dimension Mathlib.CategoryTheory.Abelian.Injective.Ext Mathlib.CategoryTheory.Abelian.Projective.Dimension Mathlib.CategoryTheory.Abelian.Projective.Ext Mathlib.CategoryTheory.Preadditive.HomOrthogonal Mathlib.CategoryTheory.Sites.SheafCohomology.Basic Mathlib.Data.Matrix.Cartan Mathlib.Data.Nat.Choose.Lucas Mathlib.Data.ZMod.Coprime Mathlib.Data.ZMod.QuotientRing Mathlib.FieldTheory.Extension Mathlib.FieldTheory.Fixed Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra Mathlib.FieldTheory.IntermediateField.Adjoin.Basic Mathlib.FieldTheory.IntermediateField.Algebraic 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.PrimeField Mathlib.FieldTheory.RatFunc.Basic Mathlib.FieldTheory.Relrank Mathlib.FieldTheory.Separable Mathlib.FieldTheory.SplittingField.Construction Mathlib.FieldTheory.SplittingField.IsSplittingField Mathlib.Geometry.Convex.Cone.TensorProduct Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField Mathlib.Geometry.RingedSpace.LocallyRingedSpace Mathlib.Geometry.RingedSpace.OpenImmersion Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing Mathlib.GroupTheory.Coxeter.Inversion Mathlib.GroupTheory.Coxeter.Length Mathlib.GroupTheory.FixedPointFree Mathlib.GroupTheory.GroupAction.Jordan Mathlib.GroupTheory.GroupAction.MultiplePrimitivity Mathlib.GroupTheory.GroupAction.MultipleTransitivity Mathlib.GroupTheory.GroupAction.SubMulAction.Combination Mathlib.GroupTheory.Perm.Cycle.Concrete Mathlib.GroupTheory.Perm.Cycle.PossibleTypes Mathlib.GroupTheory.Perm.Cycle.Type Mathlib.GroupTheory.Perm.Fin Mathlib.GroupTheory.SpecificGroups.Alternating Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional Mathlib.LinearAlgebra.AffineSpace.Matrix Mathlib.LinearAlgebra.Alternating.Uncurry.Fin Mathlib.LinearAlgebra.AnnihilatingPolynomial Mathlib.LinearAlgebra.BilinearForm.DualLattice Mathlib.LinearAlgebra.BilinearForm.Orthogonal Mathlib.LinearAlgebra.BilinearForm.Properties Mathlib.LinearAlgebra.BilinearForm.TensorProduct Mathlib.LinearAlgebra.Coevaluation Mathlib.LinearAlgebra.Contraction Mathlib.LinearAlgebra.CrossProduct Mathlib.LinearAlgebra.Dual.Lemmas Mathlib.LinearAlgebra.Eigenspace.Minpoly Mathlib.LinearAlgebra.FreeModule.Finite.Quotient Mathlib.LinearAlgebra.FreeModule.IdealQuotient Mathlib.LinearAlgebra.FreeModule.Int Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv 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.LinearMap Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly Mathlib.LinearAlgebra.Matrix.Charpoly.Univ Mathlib.LinearAlgebra.Matrix.Determinant.Basic Mathlib.LinearAlgebra.Matrix.Determinant.Misc Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular Mathlib.LinearAlgebra.Matrix.Hermitian Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber 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.Reindex Mathlib.LinearAlgebra.Matrix.SchurComplement Mathlib.LinearAlgebra.Matrix.Transvection Mathlib.LinearAlgebra.Matrix.Vec Mathlib.LinearAlgebra.Matrix.ZPow Mathlib.LinearAlgebra.PID Mathlib.LinearAlgebra.PerfectPairing.Basic Mathlib.LinearAlgebra.PerfectPairing.Restrict Mathlib.LinearAlgebra.SymplecticGroup Mathlib.LinearAlgebra.TensorProduct.Matrix Mathlib.LinearAlgebra.Trace Mathlib.LinearAlgebra.UnitaryGroup Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic Mathlib.NumberTheory.BernoulliPolynomials Mathlib.NumberTheory.Bernoulli Mathlib.NumberTheory.FLT.Basic Mathlib.NumberTheory.FLT.Four Mathlib.NumberTheory.FLT.Polynomial Mathlib.NumberTheory.KummerDedekind Mathlib.NumberTheory.PythagoreanTriples Mathlib.RepresentationTheory.Basic Mathlib.RepresentationTheory.Coinduced Mathlib.RepresentationTheory.Coinvariants Mathlib.RepresentationTheory.FiniteIndex Mathlib.RepresentationTheory.Homological.FiniteCyclic 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.Intertwining Mathlib.RepresentationTheory.Irreducible Mathlib.RepresentationTheory.Rep Mathlib.RepresentationTheory.Submodule Mathlib.RepresentationTheory.Subrepresentation Mathlib.RingTheory.Adjoin.Field Mathlib.RingTheory.Adjoin.PowerBasis Mathlib.RingTheory.AdjoinRoot Mathlib.RingTheory.Algebraic.Integral Mathlib.RingTheory.Algebraic.StronglyTranscendental Mathlib.RingTheory.AlgebraicIndependent.Adjoin Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis Mathlib.RingTheory.Binomial Mathlib.RingTheory.ClassGroup Mathlib.RingTheory.Conductor Mathlib.RingTheory.DedekindDomain.Basic Mathlib.RingTheory.DedekindDomain.Ideal.Basic Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas Mathlib.RingTheory.Derivation.MapCoeffs Mathlib.RingTheory.DiscreteValuationRing.Basic Mathlib.RingTheory.Finiteness.ModuleFinitePresentation Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra Mathlib.RingTheory.Flat.FaithfullyFlat.Descent Mathlib.RingTheory.FractionalIdeal.Extended Mathlib.RingTheory.HahnSeries.Binomial Mathlib.RingTheory.HahnSeries.Lex Mathlib.RingTheory.Henselian Mathlib.RingTheory.Ideal.AssociatedPrime.Localization Mathlib.RingTheory.Ideal.GoingDown Mathlib.RingTheory.Ideal.GoingUp Mathlib.RingTheory.Ideal.Height Mathlib.RingTheory.IntegralClosure.Algebra.Basic Mathlib.RingTheory.IntegralClosure.Algebra.Ideal Mathlib.RingTheory.IntegralClosure.GoingDown Mathlib.RingTheory.IntegralClosure.IntegrallyClosed Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic Mathlib.RingTheory.IsAdjoinRoot Mathlib.RingTheory.Jacobson.Ring Mathlib.RingTheory.KrullDimension.LocalRing Mathlib.RingTheory.KrullDimension.Module Mathlib.RingTheory.KrullDimension.NonZeroDivisors Mathlib.RingTheory.KrullDimension.PID Mathlib.RingTheory.KrullDimension.Zero Mathlib.RingTheory.LocalProperties.Basic Mathlib.RingTheory.LocalProperties.IntegrallyClosed Mathlib.RingTheory.LocalProperties.Reduced Mathlib.RingTheory.LocalRing.LocalSubring Mathlib.RingTheory.LocalRing.Quotient Mathlib.RingTheory.LocalRing.ResidueField.Basic Mathlib.RingTheory.LocalRing.ResidueField.Fiber Mathlib.RingTheory.LocalRing.ResidueField.Ideal Mathlib.RingTheory.LocalRing.ResidueField.Instances Mathlib.RingTheory.LocalRing.RingHom.Basic Mathlib.RingTheory.Localization.Away.AdjoinRoot Mathlib.RingTheory.Localization.Finiteness Mathlib.RingTheory.Localization.Free Mathlib.RingTheory.Localization.Integral Mathlib.RingTheory.Localization.Pi Mathlib.RingTheory.MatrixAlgebra Mathlib.RingTheory.MatrixPolynomialAlgebra Mathlib.RingTheory.NoetherNormalization Mathlib.RingTheory.Polynomial.Chebyshev Mathlib.RingTheory.Polynomial.Dickson Mathlib.RingTheory.Polynomial.GaussLemma Mathlib.RingTheory.Polynomial.IsIntegral Mathlib.RingTheory.Polynomial.RationalRoot Mathlib.RingTheory.Polynomial.SeparableDegree Mathlib.RingTheory.PowerBasis Mathlib.RingTheory.PowerSeries.Binomial Mathlib.RingTheory.PowerSeries.Derivative Mathlib.RingTheory.PowerSeries.Exp Mathlib.RingTheory.PowerSeries.Ideal Mathlib.RingTheory.PowerSeries.Inverse Mathlib.RingTheory.PowerSeries.WeierstrassPreparation Mathlib.RingTheory.RingHom.Bijective Mathlib.RingTheory.RingHom.FaithfullyFlat Mathlib.RingTheory.RingHom.FinitePresentation Mathlib.RingTheory.RingHom.FiniteType Mathlib.RingTheory.RingHom.Finite Mathlib.RingTheory.RingHom.Flat Mathlib.RingTheory.RingHom.Injective Mathlib.RingTheory.RingHom.Integral Mathlib.RingTheory.RingHom.Locally Mathlib.RingTheory.RingHom.OpenImmersion Mathlib.RingTheory.RingHom.Surjective Mathlib.RingTheory.RingHomProperties Mathlib.RingTheory.Smooth.IntegralClosure Mathlib.RingTheory.Spectrum.Maximal.Localization 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.RingHom Mathlib.RingTheory.Spectrum.Prime.TensorProduct Mathlib.RingTheory.Spectrum.Prime.Topology Mathlib.RingTheory.Support Mathlib.RingTheory.Valuation.AlgebraInstances Mathlib.RingTheory.Valuation.Extension Mathlib.RingTheory.Valuation.Integral Mathlib.RingTheory.Valuation.LocalSubring Mathlib.RingTheory.Valuation.Minpoly Mathlib.RingTheory.Valuation.RamificationGroup Mathlib.RingTheory.Valuation.ValuationSubring Mathlib.RingTheory.WittVector.WittPolynomial Mathlib.RingTheory.ZMod Mathlib.RingTheory.ZariskisMainTheorem
 7
11 files Mathlib.Analysis.Convex.Basic Mathlib.Analysis.Convex.Cone.Closure Mathlib.Analysis.Convex.Extreme Mathlib.Analysis.Convex.Hull Mathlib.Analysis.Convex.Join Mathlib.Analysis.Convex.Segment Mathlib.Analysis.Convex.SimplicialComplex.Basic Mathlib.Analysis.Convex.Star Mathlib.Geometry.Convex.Cone.Basic Mathlib.Geometry.Convex.Cone.Dual Mathlib.Geometry.Convex.Cone.Pointed
 8
22 files Mathlib.Algebra.Algebra.StrictPositivity Mathlib.CategoryTheory.Triangulated.Yoneda Mathlib.LinearAlgebra.AffineSpace.Basis Mathlib.LinearAlgebra.AffineSpace.Ceva Mathlib.LinearAlgebra.AffineSpace.Independent Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid Mathlib.LinearAlgebra.Alternating.DomCoprod Mathlib.LinearAlgebra.Projectivization.Cardinality Mathlib.LinearAlgebra.TensorProduct.Graded.External Mathlib.LinearAlgebra.TensorProduct.Graded.Internal Mathlib.NumberTheory.FrobeniusNumber Mathlib.RingTheory.HahnSeries.Valuation Mathlib.RingTheory.Ideal.NatInt Mathlib.RingTheory.Int.Basic Mathlib.RingTheory.Localization.Rat Mathlib.RingTheory.Valuation.Basic Mathlib.RingTheory.Valuation.ExtendToLocalization Mathlib.RingTheory.Valuation.Integers Mathlib.RingTheory.Valuation.PrimeMultiplicity Mathlib.RingTheory.Valuation.Quotient Mathlib.RingTheory.Valuation.ValuationRing
 9
388 files Mathlib.Algebra.AffineMonoid.Embedding Mathlib.Algebra.AffineMonoid.UniqueSums Mathlib.Algebra.Algebra.Epi Mathlib.Algebra.Algebra.Spectrum.Basic Mathlib.Algebra.Algebra.Spectrum.Pi Mathlib.Algebra.Algebra.Spectrum.Quasispectrum Mathlib.Algebra.Algebra.Subalgebra.IsSimpleOrder Mathlib.Algebra.Algebra.Subalgebra.Operations Mathlib.Algebra.Algebra.Subalgebra.Rank Mathlib.Algebra.AlgebraicCard Mathlib.Algebra.Azumaya.Basic Mathlib.Algebra.Category.Grp.Injective Mathlib.Algebra.Category.ModuleCat.Free Mathlib.Algebra.Category.ModuleCat.LeftResolution Mathlib.Algebra.Category.ModuleCat.Simple Mathlib.Algebra.Category.Ring.Epi Mathlib.Algebra.Category.Ring.FinitePresentation Mathlib.Algebra.Central.TensorProduct Mathlib.Algebra.CharP.IntermediateField Mathlib.Algebra.CharP.LocalRing Mathlib.Algebra.CharP.MixedCharZero Mathlib.Algebra.Colimit.Ring Mathlib.Algebra.CubicDiscriminant Mathlib.Algebra.DirectSum.Idempotents Mathlib.Algebra.DualQuaternion Mathlib.Algebra.FreeAlgebra.Cardinality Mathlib.Algebra.Group.ForwardDiff Mathlib.Algebra.Homology.ConcreteCategory Mathlib.Algebra.Homology.LocalCohomology Mathlib.Algebra.Jordan.Basic Mathlib.Algebra.Lie.Abelian Mathlib.Algebra.Lie.BaseChange Mathlib.Algebra.Lie.Character Mathlib.Algebra.Lie.Cochain 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.Semisimple.Basic Mathlib.Algebra.Lie.Semisimple.Defs Mathlib.Algebra.Lie.Sl2 Mathlib.Algebra.Lie.Solvable Mathlib.Algebra.Lie.Subalgebra Mathlib.Algebra.Lie.Submodule Mathlib.Algebra.Lie.TensorProduct Mathlib.Algebra.Lie.UniversalEnveloping Mathlib.Algebra.LinearRecurrence Mathlib.Algebra.Module.FinitePresentation Mathlib.Algebra.Module.Lattice Mathlib.Algebra.Module.Presentation.Finite Mathlib.Algebra.Module.SpanRank Mathlib.Algebra.MvPolynomial.Cardinal Mathlib.Algebra.MvPolynomial.Derivation Mathlib.Algebra.MvPolynomial.Equiv Mathlib.Algebra.MvPolynomial.Expand Mathlib.Algebra.MvPolynomial.Funext Mathlib.Algebra.MvPolynomial.Nilpotent Mathlib.Algebra.MvPolynomial.NoZeroDivisors Mathlib.Algebra.MvPolynomial.PDeriv Mathlib.Algebra.MvPolynomial.Polynomial Mathlib.Algebra.MvPolynomial.SchwartzZippel Mathlib.Algebra.Polynomial.AlgebraMap Mathlib.Algebra.Polynomial.BigOperators Mathlib.Algebra.Polynomial.CancelLeads Mathlib.Algebra.Polynomial.CoeffList Mathlib.Algebra.Polynomial.CoeffMem Mathlib.Algebra.Polynomial.Coeff Mathlib.Algebra.Polynomial.Degree.Domain Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree Mathlib.Algebra.Polynomial.Degree.Lemmas Mathlib.Algebra.Polynomial.Degree.Operations Mathlib.Algebra.Polynomial.Degree.SmallDegree Mathlib.Algebra.Polynomial.Degree.Support Mathlib.Algebra.Polynomial.Degree.TrailingDegree Mathlib.Algebra.Polynomial.Degree.Units Mathlib.Algebra.Polynomial.Derivation Mathlib.Algebra.Polynomial.Derivative Mathlib.Algebra.Polynomial.Div Mathlib.Algebra.Polynomial.EraseLead Mathlib.Algebra.Polynomial.Eval.Coeff Mathlib.Algebra.Polynomial.Eval.Degree Mathlib.Algebra.Polynomial.Eval.Irreducible Mathlib.Algebra.Polynomial.Eval.SMul Mathlib.Algebra.Polynomial.Eval.Subring Mathlib.Algebra.Polynomial.Expand Mathlib.Algebra.Polynomial.FieldDivision Mathlib.Algebra.Polynomial.GroupRingAction Mathlib.Algebra.Polynomial.HasseDeriv Mathlib.Algebra.Polynomial.Homogenize Mathlib.Algebra.Polynomial.Identities Mathlib.Algebra.Polynomial.Inductions Mathlib.Algebra.Polynomial.Laurent Mathlib.Algebra.Polynomial.Lifts Mathlib.Algebra.Polynomial.Mirror Mathlib.Algebra.Polynomial.Module.AEval Mathlib.Algebra.Polynomial.Module.Basic Mathlib.Algebra.Polynomial.Module.TensorProduct Mathlib.Algebra.Polynomial.Monic Mathlib.Algebra.Polynomial.OfFn Mathlib.Algebra.Polynomial.PartialFractions Mathlib.Algebra.Polynomial.Reverse Mathlib.Algebra.Polynomial.RingDivision Mathlib.Algebra.Polynomial.Roots Mathlib.Algebra.Polynomial.RuleOfSigns Mathlib.Algebra.Polynomial.Sequence Mathlib.Algebra.Polynomial.Smeval Mathlib.Algebra.Polynomial.SpecificDegree Mathlib.Algebra.Polynomial.Splits Mathlib.Algebra.Polynomial.SumIteratedDerivative Mathlib.Algebra.Polynomial.Taylor Mathlib.Algebra.QuadraticAlgebra.Basic Mathlib.Algebra.QuadraticAlgebra.Defs Mathlib.Algebra.QuadraticAlgebra Mathlib.Algebra.QuaternionBasis Mathlib.Algebra.Quaternion Mathlib.Algebra.Ring.Subring.IntPolynomial Mathlib.Algebra.Squarefree.Basic Mathlib.Algebra.Star.LinearMap Mathlib.Algebra.Star.UnitaryStarAlgAut Mathlib.Algebra.Star.Unitary Mathlib.Algebra.Symmetrized Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology Mathlib.CategoryTheory.Abelian.Ext Mathlib.Combinatorics.Nullstellensatz Mathlib.Data.Nat.Choose.Vandermonde Mathlib.Dynamics.Newton Mathlib.FieldTheory.Finiteness Mathlib.FieldTheory.IntermediateField.Adjoin.Defs Mathlib.FieldTheory.IntermediateField.Basic Mathlib.FieldTheory.Minpoly.Basic Mathlib.FieldTheory.MvRatFunc.Rank Mathlib.FieldTheory.Tower Mathlib.GroupTheory.FreeGroup.GeneratorEquiv Mathlib.LinearAlgebra.Alternating.Basic Mathlib.LinearAlgebra.Alternating.Curry 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.OrzechProperty 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.FreeAlgebra Mathlib.LinearAlgebra.FreeModule.Finite.Matrix Mathlib.LinearAlgebra.FreeModule.PID Mathlib.LinearAlgebra.FreeModule.StrongRankCondition Mathlib.LinearAlgebra.InvariantBasisNumber Mathlib.LinearAlgebra.LinearDisjoint Mathlib.LinearAlgebra.Matrix.Diagonal Mathlib.LinearAlgebra.Matrix.FiniteDimensional Mathlib.LinearAlgebra.Matrix.Ideal Mathlib.LinearAlgebra.Multilinear.FiniteDimensional Mathlib.LinearAlgebra.Projectivization.Action Mathlib.LinearAlgebra.Projectivization.Basic Mathlib.LinearAlgebra.Projectivization.Independence Mathlib.LinearAlgebra.Projectivization.Subspace Mathlib.LinearAlgebra.SymmetricAlgebra.Basis Mathlib.LinearAlgebra.TensorAlgebra.Basis Mathlib.LinearAlgebra.TensorProduct.Quotient Mathlib.LinearAlgebra.TensorProduct.RightExactness Mathlib.LinearAlgebra.TensorProduct.Vanishing Mathlib.ModelTheory.Algebra.Field.CharP Mathlib.ModelTheory.Algebra.Ring.FreeCommRing Mathlib.NumberTheory.Dioph Mathlib.NumberTheory.FLT.MasonStothers Mathlib.NumberTheory.PellMatiyasevic Mathlib.NumberTheory.Zsqrtd.Basic Mathlib.RepresentationTheory.Maschke Mathlib.RingTheory.AdicCompletion.Basic Mathlib.RingTheory.AdicCompletion.LocalRing Mathlib.RingTheory.AdicCompletion.Noetherian Mathlib.RingTheory.Adjoin.Dimension Mathlib.RingTheory.Adjoin.FGBaseChange Mathlib.RingTheory.Adjoin.FG Mathlib.RingTheory.Adjoin.Polynomial Mathlib.RingTheory.Adjoin.Singleton Mathlib.RingTheory.Adjoin.Tower Mathlib.RingTheory.Algebraic.Basic Mathlib.RingTheory.Algebraic.Cardinality Mathlib.RingTheory.Algebraic.Defs Mathlib.RingTheory.Algebraic.LinearIndependent Mathlib.RingTheory.Algebraic.MvPolynomial Mathlib.RingTheory.Algebraic.Pi Mathlib.RingTheory.AlgebraicIndependent.Basic Mathlib.RingTheory.AlgebraicIndependent.Transcendental Mathlib.RingTheory.Artinian.Algebra Mathlib.RingTheory.Artinian.Instances Mathlib.RingTheory.Artinian.Module Mathlib.RingTheory.Artinian.Ring Mathlib.RingTheory.Bezout Mathlib.RingTheory.Bialgebra.GroupLike Mathlib.RingTheory.Bialgebra.MonoidAlgebra Mathlib.RingTheory.Coalgebra.GroupLike Mathlib.RingTheory.Coalgebra.MonoidAlgebra Mathlib.RingTheory.Coprime.Ideal Mathlib.RingTheory.Derivation.Basic Mathlib.RingTheory.Derivation.DifferentialRing Mathlib.RingTheory.Derivation.Lie Mathlib.RingTheory.Derivation.ToSquareZero Mathlib.RingTheory.DualNumber Mathlib.RingTheory.EssentialFiniteness Mathlib.RingTheory.EuclideanDomain Mathlib.RingTheory.Filtration Mathlib.RingTheory.FiniteLength Mathlib.RingTheory.FinitePresentation Mathlib.RingTheory.FiniteStability Mathlib.RingTheory.FiniteType Mathlib.RingTheory.Finiteness.Ideal Mathlib.RingTheory.Finiteness.Nakayama Mathlib.RingTheory.Finiteness.NilpotentKer Mathlib.RingTheory.Finiteness.Nilpotent Mathlib.RingTheory.Finiteness.Quotient Mathlib.RingTheory.Finiteness.Small Mathlib.RingTheory.Flat.Basic Mathlib.RingTheory.Flat.CategoryTheory Mathlib.RingTheory.Flat.Domain Mathlib.RingTheory.Flat.Equalizer Mathlib.RingTheory.Flat.FaithfullyFlat.Basic Mathlib.RingTheory.Flat.Localization Mathlib.RingTheory.Flat.Stability Mathlib.RingTheory.FractionalIdeal.Basic Mathlib.RingTheory.FractionalIdeal.Inverse Mathlib.RingTheory.FractionalIdeal.Operations Mathlib.RingTheory.FreeCommRing Mathlib.RingTheory.GradedAlgebra.FiniteType Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization Mathlib.RingTheory.GradedAlgebra.Noetherian Mathlib.RingTheory.GradedAlgebra.Radical Mathlib.RingTheory.HahnSeries.HEval Mathlib.RingTheory.HahnSeries.PowerSeries Mathlib.RingTheory.HopfAlgebra.GroupLike Mathlib.RingTheory.HopfAlgebra.MonoidAlgebra Mathlib.RingTheory.Ideal.AssociatedPrime.Basic Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness Mathlib.RingTheory.Ideal.Basic Mathlib.RingTheory.Ideal.Colon Mathlib.RingTheory.Ideal.IdempotentFG Mathlib.RingTheory.Ideal.IsPrimary Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient Mathlib.RingTheory.Ideal.IsPrincipal Mathlib.RingTheory.Ideal.Maps Mathlib.RingTheory.Ideal.MinimalPrime.Basic Mathlib.RingTheory.Ideal.MinimalPrime.Localization Mathlib.RingTheory.Ideal.MinimalPrime.Noetherian Mathlib.RingTheory.Ideal.Oka Mathlib.RingTheory.Ideal.Operations Mathlib.RingTheory.Ideal.Over Mathlib.RingTheory.Ideal.Pointwise Mathlib.RingTheory.Ideal.Prod Mathlib.RingTheory.Ideal.Quotient.Basic Mathlib.RingTheory.Ideal.Quotient.ChineseRemainder Mathlib.RingTheory.Ideal.Quotient.Index Mathlib.RingTheory.Ideal.Quotient.Nilpotent Mathlib.RingTheory.Ideal.Quotient.Noetherian Mathlib.RingTheory.Ideal.Quotient.Operations Mathlib.RingTheory.Ideal.Quotient.PowTransition Mathlib.RingTheory.IdealFilter.Basic Mathlib.RingTheory.Idempotents Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic Mathlib.RingTheory.IsPrimary Mathlib.RingTheory.Jacobson.Ideal Mathlib.RingTheory.Jacobson.Polynomial Mathlib.RingTheory.Jacobson.Radical Mathlib.RingTheory.Jacobson.Semiprimary Mathlib.RingTheory.KrullDimension.Basic Mathlib.RingTheory.KrullDimension.Field Mathlib.RingTheory.Lasker Mathlib.RingTheory.Length Mathlib.RingTheory.LocalProperties.Exactness Mathlib.RingTheory.LocalProperties.Projective Mathlib.RingTheory.LocalProperties.Submodule Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic Mathlib.RingTheory.LocalRing.NonLocalRing Mathlib.RingTheory.LocalRing.ResidueField.Defs Mathlib.RingTheory.Localization.Algebra Mathlib.RingTheory.Localization.AsSubring Mathlib.RingTheory.Localization.AtPrime.Basic Mathlib.RingTheory.Localization.AtPrime Mathlib.RingTheory.Localization.Away.Basic Mathlib.RingTheory.Localization.Away.Lemmas Mathlib.RingTheory.Localization.BaseChange Mathlib.RingTheory.Localization.Ideal Mathlib.RingTheory.Localization.InvSubmonoid Mathlib.RingTheory.Localization.LocalizationLocalization Mathlib.RingTheory.Localization.Submodule Mathlib.RingTheory.MvPolynomial.EulerIdentity Mathlib.RingTheory.MvPolynomial.Expand Mathlib.RingTheory.MvPolynomial.FreeCommRing Mathlib.RingTheory.MvPolynomial.Groebner Mathlib.RingTheory.MvPolynomial.Homogeneous Mathlib.RingTheory.MvPolynomial.Ideal Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic Mathlib.RingTheory.MvPolynomial.Localization Mathlib.RingTheory.MvPolynomial.MonomialOrder.DegLex Mathlib.RingTheory.MvPolynomial.MonomialOrder Mathlib.RingTheory.MvPolynomial Mathlib.RingTheory.MvPowerSeries.Inverse Mathlib.RingTheory.Nakayama Mathlib.RingTheory.Nilpotent.Basic Mathlib.RingTheory.Nilpotent.Exp Mathlib.RingTheory.Nilpotent.Lemmas Mathlib.RingTheory.Noetherian.Basic Mathlib.RingTheory.Noetherian.Nilpotent Mathlib.RingTheory.Noetherian.OfPrime Mathlib.RingTheory.Noetherian.Orzech Mathlib.RingTheory.Noetherian.UniqueFactorizationDomain Mathlib.RingTheory.Polynomial.Basic Mathlib.RingTheory.Polynomial.Bernstein Mathlib.RingTheory.Polynomial.ContentIdeal Mathlib.RingTheory.Polynomial.Content Mathlib.RingTheory.Polynomial.Eisenstein.Basic Mathlib.RingTheory.Polynomial.Eisenstein.Criterion Mathlib.RingTheory.Polynomial.Eisenstein.Distinguished Mathlib.RingTheory.Polynomial.Hermite.Basic Mathlib.RingTheory.Polynomial.HilbertPoly Mathlib.RingTheory.Polynomial.Ideal Mathlib.RingTheory.Polynomial.IntegralNormalization Mathlib.RingTheory.Polynomial.IrreducibleRing Mathlib.RingTheory.Polynomial.Nilpotent Mathlib.RingTheory.Polynomial.Opposites Mathlib.RingTheory.Polynomial.Pochhammer Mathlib.RingTheory.Polynomial.Quotient Mathlib.RingTheory.Polynomial.Radical Mathlib.RingTheory.Polynomial.ScaleRoots Mathlib.RingTheory.Polynomial.ShiftedLegendre Mathlib.RingTheory.Polynomial.SmallDegreeVieta Mathlib.RingTheory.Polynomial.Tower Mathlib.RingTheory.Polynomial.UniqueFactorization Mathlib.RingTheory.Polynomial.Vieta Mathlib.RingTheory.Polynomial.Wronskian Mathlib.RingTheory.PolynomialAlgebra Mathlib.RingTheory.PolynomialLaw.Basic Mathlib.RingTheory.PowerSeries.Basic Mathlib.RingTheory.PowerSeries.Catalan Mathlib.RingTheory.PowerSeries.CoeffMulMem Mathlib.RingTheory.PowerSeries.NoZeroDivisors Mathlib.RingTheory.PowerSeries.Order Mathlib.RingTheory.PowerSeries.Schroder Mathlib.RingTheory.PowerSeries.Trunc Mathlib.RingTheory.PowerSeries.WellKnown Mathlib.RingTheory.PrincipalIdealDomainOfPrime Mathlib.RingTheory.PrincipalIdealDomain Mathlib.RingTheory.QuotSMulTop Mathlib.RingTheory.Radical Mathlib.RingTheory.ReesAlgebra Mathlib.RingTheory.Regular.Category Mathlib.RingTheory.SimpleModule.Basic Mathlib.RingTheory.SimpleModule.InjectiveProjective Mathlib.RingTheory.SimpleModule.Isotypic Mathlib.RingTheory.SimpleModule.Rank Mathlib.RingTheory.SimpleModule.WedderburnArtin Mathlib.RingTheory.SimpleRing.Matrix Mathlib.RingTheory.SimpleRing.Principal Mathlib.RingTheory.Spectrum.Prime.Basic Mathlib.RingTheory.SurjectiveOnStalks Mathlib.RingTheory.TensorProduct.DirectLimitFG Mathlib.RingTheory.TensorProduct.Finite Mathlib.RingTheory.TensorProduct.IsBaseChangeFree Mathlib.RingTheory.TensorProduct.IsBaseChangePi Mathlib.RingTheory.TensorProduct.MvPolynomial Mathlib.RingTheory.TensorProduct.Nontrivial Mathlib.RingTheory.TensorProduct.Quotient Mathlib.RingTheory.UniqueFactorizationDomain.Ideal Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky Mathlib.SetTheory.Cardinal.Free Mathlib.Tactic.ComputeDegree Mathlib.Topology.Algebra.Star.Unitary
 10
Mathlib.GroupTheory.CosetCover Mathlib.LinearAlgebra.Ray 11
111 files Mathlib.Algebra.Algebra.Subalgebra.Centralizer Mathlib.Algebra.Azumaya.Defs Mathlib.Algebra.Azumaya.Matrix Mathlib.Algebra.Category.AlgCat.Limits Mathlib.Algebra.Category.BialgCat.Basic Mathlib.Algebra.Category.BialgCat.Monoidal Mathlib.Algebra.Category.Grp.AB Mathlib.Algebra.Category.Grp.Abelian Mathlib.Algebra.Category.Grp.Images Mathlib.Algebra.Category.Grp.IsFinite Mathlib.Algebra.Category.HopfAlgCat.Basic Mathlib.Algebra.Category.HopfAlgCat.Monoidal Mathlib.Algebra.Category.ModuleCat.AB Mathlib.Algebra.Category.ModuleCat.Abelian Mathlib.Algebra.Category.ModuleCat.Biproducts Mathlib.Algebra.Category.ModuleCat.Images Mathlib.Algebra.Category.ModuleCat.Localization Mathlib.Algebra.Category.ModuleCat.Presheaf.Abelian Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback 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.PullbackFree Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent Mathlib.Algebra.DirectSum.Internal Mathlib.Algebra.Group.UniqueProds.VectorSpace Mathlib.Algebra.Homology.ShortComplex.Ab Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory Mathlib.Algebra.Homology.ShortComplex.ModuleCat Mathlib.Algebra.Module.GradedModule Mathlib.Algebra.MonoidAlgebra.Grading Mathlib.Analysis.Normed.Lp.WithLp Mathlib.Analysis.Subadditive 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.Galois.Equivalence Mathlib.CategoryTheory.Galois.EssSurj Mathlib.CategoryTheory.Galois.IsFundamentalgroup Mathlib.CategoryTheory.Preadditive.Yoneda.Limits Mathlib.CategoryTheory.Sites.MayerVietorisSquare Mathlib.Geometry.Manifold.ChartedSpace Mathlib.Geometry.Manifold.HasGroupoid Mathlib.Geometry.Manifold.LocalInvariantProperties Mathlib.Geometry.Manifold.Sheaf.Basic Mathlib.Geometry.Manifold.StructureGroupoid Mathlib.LinearAlgebra.Basis.VectorSpace Mathlib.LinearAlgebra.FreeModule.Finite.Basic Mathlib.LinearAlgebra.FreeProduct.Basic Mathlib.LinearAlgebra.Matrix.Dual Mathlib.LinearAlgebra.Matrix.ToLin Mathlib.LinearAlgebra.PiTensorProduct.Dual Mathlib.LinearAlgebra.TensorAlgebra.Grading Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower Mathlib.LinearAlgebra.TensorProduct.Subalgebra Mathlib.LinearAlgebra.TensorProduct.Submodule Mathlib.MeasureTheory.OuterMeasure.Defs Mathlib.RingTheory.Bialgebra.Basic Mathlib.RingTheory.Bialgebra.Equiv Mathlib.RingTheory.Bialgebra.Hom Mathlib.RingTheory.Bialgebra.TensorProduct Mathlib.RingTheory.Coalgebra.Convolution Mathlib.RingTheory.Finiteness.Cardinality Mathlib.RingTheory.Finiteness.Projective Mathlib.RingTheory.GradedAlgebra.Basic Mathlib.RingTheory.GradedAlgebra.Homogeneous.Submodule Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring Mathlib.RingTheory.HopfAlgebra.Basic Mathlib.RingTheory.HopfAlgebra.TensorProduct Mathlib.RingTheory.MvPolynomial.Basic Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous Mathlib.RingTheory.OrzechProperty Mathlib.RingTheory.TensorProduct.Free Mathlib.Topology.Algebra.ClopenNhdofOne Mathlib.Topology.Algebra.Field Mathlib.Topology.Algebra.LinearTopology Mathlib.Topology.Algebra.Localization Mathlib.Topology.Algebra.MetricSpace.Lipschitz Mathlib.Topology.Algebra.Nonarchimedean.Basic Mathlib.Topology.Algebra.Nonarchimedean.Completion Mathlib.Topology.Algebra.Nonarchimedean.TotallyDisconnected Mathlib.Topology.Algebra.OpenSubgroup Mathlib.Topology.Algebra.Order.Field Mathlib.Topology.Algebra.Order.LiminfLimsup Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace Mathlib.Topology.Algebra.Ring.Basic Mathlib.Topology.Algebra.Ring.Ideal Mathlib.Topology.Algebra.Ring.Real Mathlib.Topology.Algebra.UniformField Mathlib.Topology.Algebra.UniformRing Mathlib.Topology.Category.TopCommRingCat Mathlib.Topology.Connected.LocPathConnected Mathlib.Topology.Connected.PathComponentOne Mathlib.Topology.Connected.PathConnected Mathlib.Topology.Homotopy.Basic Mathlib.Topology.Homotopy.Equiv Mathlib.Topology.Homotopy.HSpaces Mathlib.Topology.Instances.Rat Mathlib.Topology.Instances.ZMultiples Mathlib.Topology.Path Mathlib.Topology.Sheaves.MayerVietoris Mathlib.Topology.UniformSpace.CompareReals Mathlib.Topology.UniformSpace.Path Mathlib.Topology.UnitInterval
 12
95 files Mathlib.Algebra.Category.CoalgCat.Basic Mathlib.Algebra.Category.CoalgCat.ComonEquivalence Mathlib.Algebra.Category.CoalgCat.Monoidal Mathlib.Algebra.Category.ModuleCat.Adjunctions Mathlib.Algebra.Category.ModuleCat.ChangeOfRings Mathlib.Algebra.Category.ModuleCat.Limits 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.Sheafify Mathlib.Algebra.Category.ModuleCat.Presheaf Mathlib.Algebra.Category.ModuleCat.Products Mathlib.Algebra.Category.ModuleCat.Projective Mathlib.Algebra.Category.ModuleCat.Pseudofunctor Mathlib.Algebra.Category.ModuleCat.Sheaf.ChangeOfRings Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous Mathlib.Algebra.Category.ModuleCat.Sheaf Mathlib.Algebra.Colimit.Finiteness Mathlib.Algebra.Colimit.Module Mathlib.Algebra.Colimit.TensorProduct Mathlib.Algebra.DirectSum.Algebra Mathlib.Algebra.DirectSum.Decomposition Mathlib.Algebra.DirectSum.Finsupp Mathlib.Algebra.DirectSum.Module Mathlib.Algebra.Module.Presentation.DirectSum Mathlib.Algebra.Module.Presentation.Free Mathlib.Algebra.Module.Presentation.RestrictScalars Mathlib.Algebra.Module.Projective Mathlib.Algebra.MonoidAlgebra.ToDirectSum Mathlib.CategoryTheory.Galois.Topology Mathlib.GroupTheory.Coxeter.Basic Mathlib.LinearAlgebra.DFinsupp Mathlib.LinearAlgebra.DirectSum.Basis Mathlib.LinearAlgebra.DirectSum.Finite Mathlib.LinearAlgebra.DirectSum.Finsupp Mathlib.LinearAlgebra.DirectSum.TensorProduct Mathlib.LinearAlgebra.Finsupp.VectorSpace Mathlib.LinearAlgebra.LinearIndependent.Lemmas Mathlib.LinearAlgebra.Matrix.StdBasis Mathlib.LinearAlgebra.Multilinear.Basis Mathlib.LinearAlgebra.Multilinear.DFinsupp Mathlib.LinearAlgebra.Multilinear.DirectSum Mathlib.LinearAlgebra.Multilinear.Finsupp Mathlib.LinearAlgebra.PiTensorProduct.Basis Mathlib.LinearAlgebra.PiTensorProduct.DFinsupp Mathlib.LinearAlgebra.PiTensorProduct.DirectSum Mathlib.LinearAlgebra.PiTensorProduct.Finsupp Mathlib.LinearAlgebra.SesquilinearForm.Basic Mathlib.LinearAlgebra.SesquilinearForm Mathlib.LinearAlgebra.StdBasis Mathlib.LinearAlgebra.TensorPower.Basic Mathlib.LinearAlgebra.TensorPower.Pairing Mathlib.LinearAlgebra.TensorProduct.Basis Mathlib.LinearAlgebra.TensorProduct.DirectLimit 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.Morita.Basic Mathlib.RingTheory.Morita.Matrix Mathlib.Topology.Algebra.Equicontinuity Mathlib.Topology.Algebra.Group.Basic Mathlib.Topology.Algebra.Group.ClosedSubgroup Mathlib.Topology.Algebra.Group.Compact Mathlib.Topology.Algebra.Group.GroupTopology Mathlib.Topology.Algebra.Group.OpenMapping Mathlib.Topology.Algebra.Group.Pointwise Mathlib.Topology.Algebra.Group.Quotient Mathlib.Topology.Algebra.Group.SubmonoidClosure Mathlib.Topology.Algebra.Group.TopologicalAbelianization Mathlib.Topology.Algebra.GroupCompletion Mathlib.Topology.Algebra.InfiniteSum.Constructions Mathlib.Topology.Algebra.InfiniteSum.GroupCompletion Mathlib.Topology.Algebra.InfiniteSum.Group Mathlib.Topology.Algebra.InfiniteSum.NatInt Mathlib.Topology.Algebra.InfiniteSum.UniformOn Mathlib.Topology.Algebra.IsUniformGroup.Basic Mathlib.Topology.Algebra.IsUniformGroup.Constructions Mathlib.Topology.Algebra.IsUniformGroup.Defs Mathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup Mathlib.Topology.Algebra.IsUniformGroup.Order Mathlib.Topology.Algebra.Order.UpperLower Mathlib.Topology.Algebra.ProperAction.AddTorsor Mathlib.Topology.Algebra.ProperAction.Basic Mathlib.Topology.Algebra.UniformConvergence Mathlib.Topology.Algebra.UniformMulAction Mathlib.Topology.Covering.Quotient Mathlib.Topology.UniformSpace.Matrix
 13
3 files Mathlib.GroupTheory.Perm.ConjAct Mathlib.GroupTheory.Perm.Cycle.Factors Mathlib.NumberTheory.ClassNumber.AdmissibleAbs
 14
5 files Mathlib.RingTheory.MvPowerSeries.Basic Mathlib.RingTheory.MvPowerSeries.LexOrder Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors Mathlib.RingTheory.MvPowerSeries.Order Mathlib.RingTheory.MvPowerSeries.Trunc
 15
4 files Mathlib.Algebra.CharP.Algebra Mathlib.Algebra.CharP.Subring Mathlib.Algebra.Homology.AlternatingConst Mathlib.Algebra.Module.LocalizedModule.Submodule
 16
9 files Mathlib.FieldTheory.RatFunc.Defs Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup Mathlib.LinearAlgebra.AffineSpace.Centroid Mathlib.LinearAlgebra.AffineSpace.Combination Mathlib.LinearAlgebra.AffineSpace.Ordered Mathlib.LinearAlgebra.AffineSpace.Slope Mathlib.RingTheory.HahnSeries.Cardinal Mathlib.RingTheory.HahnSeries.Summable Mathlib.RingTheory.Localization.Module
 17
4 files Mathlib.LinearAlgebra.SymmetricAlgebra.Basic Mathlib.LinearAlgebra.TensorAlgebra.Basic Mathlib.RingTheory.Congruence.Hom Mathlib.RingTheory.Finiteness.Subalgebra
 18
5 files Mathlib.Algebra.Module.LocalizedModule.Int Mathlib.Algebra.Order.Chebyshev Mathlib.Data.Matrix.ColumnRowPartitioned Mathlib.RingTheory.Finiteness.Finsupp Mathlib.RingTheory.Ideal.Basis
 19
Mathlib.LinearAlgebra.Matrix.SemiringInverse 20
4 files Mathlib.Algebra.BigOperators.Balance Mathlib.Algebra.BigOperators.Expect Mathlib.GroupTheory.Perm.Closure Mathlib.GroupTheory.Perm.Cycle.Basic
 21
Mathlib.GroupTheory.GroupAction.Iwasawa Mathlib.GroupTheory.GroupAction.Primitive 24
4 files Mathlib.RingTheory.Finiteness.Basic Mathlib.RingTheory.Finiteness.Lattice Mathlib.RingTheory.Noetherian.Defs Mathlib.RingTheory.Noetherian.Filter
 26
Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem 27
3 files Mathlib.Algebra.Module.LocalizedModule.Exact Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue Mathlib.Tactic.Module
 28
5 files Mathlib.Algebra.Polynomial.Cardinal Mathlib.Computability.TMComputable Mathlib.LinearAlgebra.Dimension.Basic Mathlib.LinearAlgebra.Dimension.Finrank Mathlib.LinearAlgebra.Dimension.Subsingleton
 32
3 files Mathlib.Combinatorics.SimpleGraph.AdjMatrix Mathlib.Combinatorics.SimpleGraph.StronglyRegular Mathlib.LinearAlgebra.Basis.Cardinality
 33
Mathlib.Data.Finsupp.MonomialOrder.DegLex Mathlib.Topology.Algebra.Affine 34
7 files Mathlib.LinearAlgebra.AffineSpace.AffineEquiv Mathlib.LinearAlgebra.AffineSpace.AffineMap Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic Mathlib.LinearAlgebra.AffineSpace.MidpointZero Mathlib.LinearAlgebra.AffineSpace.Midpoint Mathlib.LinearAlgebra.AffineSpace.Pointwise Mathlib.LinearAlgebra.AffineSpace.Restrict
 36
52 files Mathlib.Algebra.Algebra.Operations Mathlib.Algebra.Algebra.Subalgebra.Directed Mathlib.Algebra.Algebra.Subalgebra.Lattice Mathlib.Algebra.Algebra.Subalgebra.MulOpposite Mathlib.Algebra.Algebra.Subalgebra.Pi Mathlib.Algebra.Algebra.Subalgebra.Pointwise Mathlib.Algebra.Algebra.Subalgebra.Prod Mathlib.Algebra.Algebra.Subalgebra.Tower Mathlib.Algebra.Algebra.Subalgebra.Unitization Mathlib.Algebra.Category.AlgCat.Basic Mathlib.Algebra.Category.AlgCat.Monoidal Mathlib.Algebra.Category.AlgCat.Symmetric Mathlib.Algebra.Category.Ring.Adjunctions Mathlib.Algebra.Central.Basic Mathlib.Algebra.Central.Defs Mathlib.Algebra.Central.End Mathlib.Algebra.Central.Matrix Mathlib.Algebra.DualNumber Mathlib.Algebra.FreeAlgebra Mathlib.Algebra.Module.Bimodule 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.Invertible Mathlib.Algebra.MvPolynomial.Monad Mathlib.Algebra.MvPolynomial.Rename Mathlib.Algebra.MvPolynomial.Supported Mathlib.Algebra.MvPolynomial.Variables Mathlib.Algebra.Star.Free Mathlib.Algebra.Star.Subalgebra Mathlib.Algebra.TrivSqZeroExt Mathlib.Algebra.Vertex.HVertexOperator Mathlib.Algebra.Vertex.VertexOperator Mathlib.CategoryTheory.Monoidal.Internal.Module Mathlib.Data.Matrix.DualNumber Mathlib.LinearAlgebra.SModEq.Pointwise Mathlib.LinearAlgebra.TensorProduct.Opposite Mathlib.RingTheory.Adjoin.Basic Mathlib.RingTheory.AlgebraicIndependent.Defs Mathlib.RingTheory.HahnSeries.Multiplication Mathlib.RingTheory.IsTensorProduct Mathlib.RingTheory.MvPolynomial.Symmetric.Defs Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities Mathlib.RingTheory.MvPolynomial.Tower Mathlib.RingTheory.TensorProduct.Basic Mathlib.RingTheory.TensorProduct.Maps Mathlib.RingTheory.TensorProduct.MonoidAlgebra Mathlib.RingTheory.TensorProduct.Pi
 37
Mathlib.Combinatorics.SimpleGraph.Hall 39
4 files Mathlib.Combinatorics.SimpleGraph.Matching Mathlib.Combinatorics.SimpleGraph.Tutte Mathlib.Combinatorics.SimpleGraph.UniversalVerts Mathlib.LinearAlgebra.Basis.Flag
 40
6 files Mathlib.Algebra.Module.Presentation.Tensor Mathlib.Data.Matrix.Invertible Mathlib.LinearAlgebra.BilinearForm.Hom Mathlib.LinearAlgebra.Matrix.Circulant Mathlib.LinearAlgebra.SModEq.Basic Mathlib.LinearAlgebra.SModEq
 41
Mathlib.Algebra.Category.ModuleCat.Colimits Mathlib.Algebra.Category.ModuleCat.FilteredColimits 42
3 files Mathlib.RingTheory.IntegralClosure.Algebra.Defs Mathlib.RingTheory.IntegralClosure.IsIntegral.Defs Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Defs
 43
Mathlib.Algebra.Polynomial.Degree.Definitions Mathlib.Algebra.Polynomial.Degree.Monomial 44
Mathlib.Algebra.SkewMonoidAlgebra.Support 46
21 files Mathlib.Algebra.Polynomial.Basic Mathlib.Algebra.Polynomial.Basis Mathlib.Algebra.Polynomial.Eval.Algebra Mathlib.Algebra.Polynomial.Eval.Defs Mathlib.Algebra.Polynomial.Monomial Mathlib.Algebra.SkewMonoidAlgebra.Basic Mathlib.Algebra.SkewMonoidAlgebra.Lift Mathlib.Algebra.SkewMonoidAlgebra.Single Mathlib.Algebra.SkewPolynomial.Basic Mathlib.Data.Finsupp.Weight Mathlib.LinearAlgebra.Basis.Basic Mathlib.LinearAlgebra.Basis.Exact Mathlib.LinearAlgebra.Basis.Fin Mathlib.LinearAlgebra.Basis.Prod Mathlib.LinearAlgebra.Basis.SMul Mathlib.LinearAlgebra.Basis.Submodule Mathlib.LinearAlgebra.Countable Mathlib.LinearAlgebra.FreeModule.Basic Mathlib.LinearAlgebra.Matrix.DotProduct Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs Mathlib.RingTheory.AlgebraTower
 47
23 files Mathlib.Algebra.FreeNonUnitalNonAssocAlgebra Mathlib.Algebra.Module.Presentation.Basic Mathlib.Algebra.Module.Presentation.Cokernel Mathlib.Algebra.Module.Presentation.Tautological Mathlib.Algebra.Module.Submodule.Pointwise Mathlib.Algebra.MonoidAlgebra.Basic Mathlib.Algebra.MonoidAlgebra.Degree Mathlib.Algebra.MonoidAlgebra.Support Mathlib.Combinatorics.Optimization.ValuedCSP Mathlib.Data.Matrix.Block Mathlib.Data.Matrix.Reflection Mathlib.GroupTheory.Coxeter.Matrix Mathlib.LinearAlgebra.Finsupp.Pi Mathlib.LinearAlgebra.LinearIndependent.Basic Mathlib.LinearAlgebra.LinearIndependent.Defs Mathlib.LinearAlgebra.Matrix.ConjTranspose Mathlib.LinearAlgebra.Matrix.Hadamard Mathlib.LinearAlgebra.Matrix.Notation Mathlib.LinearAlgebra.Matrix.Permanent Mathlib.LinearAlgebra.Matrix.RowCol Mathlib.LinearAlgebra.Matrix.Symmetric Mathlib.LinearAlgebra.Matrix.Trace Mathlib.Topology.Algebra.Monoid.FunOnFinite
 48
8 files Mathlib.Algebra.MonoidAlgebra.Module Mathlib.LinearAlgebra.Basis.Bilinear Mathlib.LinearAlgebra.Basis.Defs Mathlib.LinearAlgebra.Dual.Basis Mathlib.LinearAlgebra.Finsupp.LSum Mathlib.LinearAlgebra.Finsupp.LinearCombination Mathlib.LinearAlgebra.Finsupp.Supported Mathlib.LinearAlgebra.Matrix.Integer
 49
Mathlib.Algebra.Category.Grp.Colimits 50
Mathlib.LinearAlgebra.Isomorphisms 52
Mathlib.Algebra.Algebra.Subalgebra.Matrix Mathlib.Data.Matrix.Bilinear 54
Mathlib.GroupTheory.ClassEquation 58
7 files Mathlib.Data.Matrix.Basic Mathlib.Data.Matrix.Basis Mathlib.Data.Matrix.Composition Mathlib.Data.Set.Card.Arithmetic Mathlib.Data.Setoid.Partition.Card Mathlib.LinearAlgebra.Matrix.Module Mathlib.LinearAlgebra.Matrix.Unique
 61
8 files Mathlib.LinearAlgebra.Multilinear.Basic Mathlib.LinearAlgebra.Multilinear.Curry Mathlib.LinearAlgebra.Multilinear.Pi Mathlib.LinearAlgebra.Multilinear.TensorProduct Mathlib.LinearAlgebra.PiTensorProduct Mathlib.LinearAlgebra.TensorPower.Symmetric Mathlib.RingTheory.PiTensorProduct Mathlib.Topology.Algebra.WithZeroTopology
 62
Mathlib.CategoryTheory.Preadditive.Mat 63
10 files Mathlib.Algebra.Category.Grp.Subobject Mathlib.Algebra.Category.ModuleCat.EpiMono Mathlib.Algebra.Category.ModuleCat.Injective Mathlib.Algebra.Category.ModuleCat.Kernels Mathlib.Algebra.Category.ModuleCat.Subobject Mathlib.Algebra.Module.Injective Mathlib.CategoryTheory.Abelian.Pseudoelements Mathlib.CategoryTheory.Preadditive.Yoneda.Injective Mathlib.CategoryTheory.Preadditive.Yoneda.Projective Mathlib.LinearAlgebra.TensorProduct.Pi
 64
Mathlib.Combinatorics.Pigeonhole 67
Mathlib.Topology.LocallyConstant.Algebra 69
10 files Mathlib.Algebra.Exact Mathlib.Algebra.FiveLemma Mathlib.Algebra.Module.SnakeLemma Mathlib.Combinatorics.Enumerative.IncidenceAlgebra Mathlib.LinearAlgebra.Goursat Mathlib.LinearAlgebra.LeftExact Mathlib.LinearAlgebra.Pi Mathlib.LinearAlgebra.Projection Mathlib.LinearAlgebra.Quotient.Basic Mathlib.LinearAlgebra.Quotient.Pi
 71
12 files Mathlib.Combinatorics.SimpleGraph.IncMatrix Mathlib.Data.Matrix.Action Mathlib.Data.Matrix.Mul Mathlib.Data.Matrix.PEquiv Mathlib.Dynamics.Flow Mathlib.Dynamics.OmegaLimit Mathlib.LinearAlgebra.Matrix.Irreducible.Defs Mathlib.LinearAlgebra.Matrix.Orthogonal Mathlib.Topology.Algebra.Group.AddTorsor Mathlib.Topology.Algebra.GroupWithZero Mathlib.Topology.Algebra.Monoid Mathlib.Topology.ApproximateUnit
 74
Mathlib.Algebra.DirectSum.AddChar Mathlib.Combinatorics.Enumerative.InclusionExclusion 75
Mathlib.Algebra.DirectSum.Ring 78
4 files Mathlib.Data.DFinsupp.Interval Mathlib.Data.Multiset.Interval Mathlib.Topology.Algebra.InfiniteSum.Basic Mathlib.Topology.Algebra.InfiniteSum.Defs
 83
Mathlib.Algebra.Module.BigOperators 86
Mathlib.Algebra.DirectSum.Basic Mathlib.Data.DFinsupp.Multiset 89
3 files Mathlib.Algebra.BigOperators.GroupWithZero.Action Mathlib.Data.DFinsupp.BigOperators Mathlib.Data.DFinsupp.Submonoid
 90
Mathlib.Algebra.BigOperators.Finprod 92

Declarations diff

+ finprod_le_finprod
+ finprod_le_finprod'
+ le_mul_max_max_left
+ le_mul_max_max_right
+ le_prod_max_one
+ logHeight₁_add_le
+ logHeight₁_sum_le
+ max_abv_add_one_le
+ max_abv_add_one_le_of_nonarch
+ max_abv_sum_one_le
+ max_abv_sum_one_le_of_nonarch
+ mulHeight₁_add_le
+ mulHeight₁_sum_le
+ one_le_mul_max_max
+ prod_map_prod

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

@github-actions github-actions bot removed the awaiting-CI This PR doesn't pass CI yet. This label is automatically removed once it does. label Jan 23, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

large-import Automatically added label for PRs with a significant increase in transitive imports t-number-theory Number theory (also use t-algebra or t-analysis to specialize)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@MichaelStollBayreuth