refactor: make `MonoidAlgebra` into a one-field structure by YaelDillies · Pull Request #25273 · leanprover-community/mathlib4

YaelDillies · 2025-05-28T17:48:32Z

github-actions · 2025-05-28T17:49:38Z

PR summary 044631201f

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Algebra.Polynomial.Cardinal	1000	1002	+2 (+0.20%)
Mathlib.Algebra.MonoidAlgebra.Opposite	684	685	+1 (+0.15%)
Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors	698	699	+1 (+0.14%)
Mathlib.Algebra.MonoidAlgebra.Module	936	937	+1 (+0.11%)
Mathlib.Algebra.MonoidAlgebra.Support	942	943	+1 (+0.11%)
Mathlib.Algebra.MonoidAlgebra.Degree	949	950	+1 (+0.11%)
Mathlib.Algebra.Polynomial.Basic	951	952	+1 (+0.11%)
Mathlib.Algebra.Polynomial.Basis	952	953	+1 (+0.11%)
Mathlib.Algebra.Polynomial.Degree.Defs	967	968	+1 (+0.10%)
Mathlib.Algebra.Polynomial.Coeff	1027	1028	+1 (+0.10%)
Mathlib.Algebra.Polynomial.Eval.Coeff	1029	1030	+1 (+0.10%)
Mathlib.RingTheory.Finiteness.Finsupp	1029	1030	+1 (+0.10%)
Mathlib.Algebra.Polynomial.Derivative	1044	1045	+1 (+0.10%)
Mathlib.Algebra.Polynomial.Reverse	1058	1059	+1 (+0.09%)
Mathlib.Algebra.Polynomial.UnitTrinomial	1062	1063	+1 (+0.09%)
Mathlib.LinearAlgebra.Finsupp.VectorSpace	1067	1068	+1 (+0.09%)
Mathlib.Algebra.Polynomial.HasseDeriv	1080	1081	+1 (+0.09%)
Mathlib.Algebra.Polynomial.OfFn	1091	1092	+1 (+0.09%)
Mathlib.RingTheory.TensorProduct.Free	1142	1143	+1 (+0.09%)
Mathlib.RingTheory.TensorProduct.MvPolynomial	1212	1213	+1 (+0.08%)
Mathlib.Algebra.FreeAlgebra.Cardinality	1233	1234	+1 (+0.08%)
Mathlib.RingTheory.Extension.Generators	1572	1573	+1 (+0.06%)
Mathlib.RingTheory.Derivation.MapCoeffs	1633	1634	+1 (+0.06%)
Mathlib.RingTheory.Polynomial.IsIntegral	1656	1657	+1 (+0.06%)
Mathlib.FieldTheory.Finite.Polynomial	1720	1721	+1 (+0.06%)
Mathlib.RingTheory.Spectrum.Prime.Polynomial	1866	1867	+1 (+0.05%)
Mathlib.RingTheory.LaurentSeries	2271	2272	+1 (+0.04%)

Import changes for all files

Files	Import difference
1313 files `Mathlib.Algebra.AffineMonoid.Embedding` `Mathlib.Algebra.AffineMonoid.UniqueSums` `Mathlib.Algebra.Algebra.Subalgebra.Centralizer` `Mathlib.Algebra.AlgebraicCard` `Mathlib.Algebra.Azumaya.Defs` `Mathlib.Algebra.Azumaya.Matrix` `Mathlib.Algebra.Category.ContinuousCohomology.Basic` `Mathlib.Algebra.Category.ModuleCat.Descent` `Mathlib.Algebra.Category.ModuleCat.Ext.DimensionShifting` `Mathlib.Algebra.Category.ModuleCat.Ext.Finite` `Mathlib.Algebra.Category.ModuleCat.Ext.HasExt` `Mathlib.Algebra.Category.ModuleCat.Free` `Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension` `Mathlib.Algebra.Category.ModuleCat.Projective` `Mathlib.Algebra.Category.ModuleCat.Simple` `Mathlib.Algebra.Category.ModuleCat.Topology.Basic` `Mathlib.Algebra.Category.ModuleCat.Topology.Homology` `Mathlib.Algebra.Category.ModuleCat.Ulift` `Mathlib.Algebra.Category.Ring.EqualizerPushout` `Mathlib.Algebra.Category.Ring.Under.Limits` `Mathlib.Algebra.DualQuaternion` `Mathlib.Algebra.FreeAlgebra.Cardinality` `Mathlib.Algebra.GCDMonoid.IntegrallyClosed` `Mathlib.Algebra.Group.ForwardDiff` `Mathlib.Algebra.Homology.LocalCohomology` `Mathlib.Algebra.Jordan.Basic` `Mathlib.Algebra.Lie.Abelian` `Mathlib.Algebra.Lie.AdjointAction.Basic` `Mathlib.Algebra.Lie.AdjointAction.Derivation` `Mathlib.Algebra.Lie.BaseChange` `Mathlib.Algebra.Lie.Basis` `Mathlib.Algebra.Lie.CartanExists` `Mathlib.Algebra.Lie.Cochain` `Mathlib.Algebra.Lie.Derivation.Basic` `Mathlib.Algebra.Lie.Derivation.Killing` `Mathlib.Algebra.Lie.DirectSum` `Mathlib.Algebra.Lie.EngelSubalgebra` `Mathlib.Algebra.Lie.Engel` `Mathlib.Algebra.Lie.Extension` `Mathlib.Algebra.Lie.Graded` `Mathlib.Algebra.Lie.IdealOperations` `Mathlib.Algebra.Lie.Ideal` `Mathlib.Algebra.Lie.Killing` `Mathlib.Algebra.Lie.LieTheorem` `Mathlib.Algebra.Lie.Normalizer` `Mathlib.Algebra.Lie.OfAssociative` `Mathlib.Algebra.Lie.Prod` `Mathlib.Algebra.Lie.Quotient` `Mathlib.Algebra.Lie.Rank` `Mathlib.Algebra.Lie.SemiDirect` `Mathlib.Algebra.Lie.Semisimple.Lemmas` `Mathlib.Algebra.Lie.Subalgebra` `Mathlib.Algebra.Lie.Submodule` `Mathlib.Algebra.Lie.TensorProduct` `Mathlib.Algebra.Lie.TraceForm` `Mathlib.Algebra.Lie.Weights.Basic` `Mathlib.Algebra.Lie.Weights.Cartan` `Mathlib.Algebra.Lie.Weights.Chain` `Mathlib.Algebra.Lie.Weights.IsSimple` `Mathlib.Algebra.Lie.Weights.Killing` `Mathlib.Algebra.Lie.Weights.Linear` `Mathlib.Algebra.Lie.Weights.RootSystem` `Mathlib.Algebra.LinearRecurrence` `Mathlib.Algebra.Module.DedekindDomain` `Mathlib.Algebra.Module.FinitePresentation` `Mathlib.Algebra.Module.Lattice` `Mathlib.Algebra.Module.LinearMap.Polynomial` `Mathlib.Algebra.Module.PID` `Mathlib.Algebra.Module.Presentation.Differentials` `Mathlib.Algebra.Module.Presentation.Finite` `Mathlib.Algebra.Module.Presentation.Free` `Mathlib.Algebra.Module.Projective` `Mathlib.Algebra.Module.SpanRank` `Mathlib.Algebra.Module.Torsion.PrimaryComponent` `Mathlib.Algebra.MonoidAlgebra.Degree` `Mathlib.Algebra.MonoidAlgebra.Module` `Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors` `Mathlib.Algebra.MonoidAlgebra.Opposite` `Mathlib.Algebra.MonoidAlgebra.Support` `Mathlib.Algebra.Order.Ring.StandardPart` `Mathlib.Algebra.Polynomial.Basic` `Mathlib.Algebra.Polynomial.Basis` `Mathlib.Algebra.Polynomial.BigOperators` `Mathlib.Algebra.Polynomial.Bivariate` `Mathlib.Algebra.Polynomial.CancelLeads` `Mathlib.Algebra.Polynomial.CoeffList` `Mathlib.Algebra.Polynomial.CoeffMem` `Mathlib.Algebra.Polynomial.Coeff` `Mathlib.Algebra.Polynomial.Degree.Definitions` `Mathlib.Algebra.Polynomial.Degree.Defs` `Mathlib.Algebra.Polynomial.Degree.Domain` `Mathlib.Algebra.Polynomial.Degree.Lemmas` `Mathlib.Algebra.Polynomial.Degree.Monomial` `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.DenomsClearable` `Mathlib.Algebra.Polynomial.Derivative` `Mathlib.Algebra.Polynomial.Div` `Mathlib.Algebra.Polynomial.EraseLead` `Mathlib.Algebra.Polynomial.Eval.Algebra` `Mathlib.Algebra.Polynomial.Eval.Coeff` `Mathlib.Algebra.Polynomial.Eval.Defs` `Mathlib.Algebra.Polynomial.Eval.Degree` `Mathlib.Algebra.Polynomial.Eval.Irreducible` `Mathlib.Algebra.Polynomial.Eval.SMul` `Mathlib.Algebra.Polynomial.Eval.Subring` `Mathlib.Algebra.Polynomial.HasseDeriv` `Mathlib.Algebra.Polynomial.Identities` `Mathlib.Algebra.Polynomial.Inductions` `Mathlib.Algebra.Polynomial.Mirror` `Mathlib.Algebra.Polynomial.Module.FiniteDimensional` `Mathlib.Algebra.Polynomial.Monic` `Mathlib.Algebra.Polynomial.Monomial` `Mathlib.Algebra.Polynomial.OfFn` `Mathlib.Algebra.Polynomial.PartialFractions` `Mathlib.Algebra.Polynomial.Reverse` `Mathlib.Algebra.Polynomial.UnitTrinomial` `Mathlib.Algebra.QuadraticAlgebra.Basic` `Mathlib.Algebra.QuadraticAlgebra.Defs` `Mathlib.Algebra.QuadraticAlgebra` `Mathlib.Algebra.QuaternionBasis` `Mathlib.Algebra.Quaternion` `Mathlib.Algebra.Star.LinearMap` `Mathlib.Algebra.Symmetrized` `Mathlib.AlgebraicGeometry.AffineScheme` `Mathlib.AlgebraicGeometry.AffineSpace` `Mathlib.AlgebraicGeometry.AffineTransitionLimit` `Mathlib.AlgebraicGeometry.AlgClosed.Basic` `Mathlib.AlgebraicGeometry.Artinian` `Mathlib.AlgebraicGeometry.ColimitsOver` `Mathlib.AlgebraicGeometry.Cover.Directed` `Mathlib.AlgebraicGeometry.Cover.MorphismProperty` `Mathlib.AlgebraicGeometry.Cover.Open` `Mathlib.AlgebraicGeometry.Cover.Over` `Mathlib.AlgebraicGeometry.Cover.QuasiCompact` `Mathlib.AlgebraicGeometry.Cover.Sigma` `Mathlib.AlgebraicGeometry.EffectiveEpi` `Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic` `Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula` `Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point` `Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic` `Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree` `Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ` `Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic` `Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula` `Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point` `Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic` `Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula` `Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point` `Mathlib.AlgebraicGeometry.EllipticCurve.Reduction` `Mathlib.AlgebraicGeometry.Fiber` `Mathlib.AlgebraicGeometry.FunctionField` `Mathlib.AlgebraicGeometry.GammaSpecAdjunction` `Mathlib.AlgebraicGeometry.Geometrically.Basic` `Mathlib.AlgebraicGeometry.Geometrically.Integral` `Mathlib.AlgebraicGeometry.Geometrically.Irreducible` `Mathlib.AlgebraicGeometry.Geometrically.Reduced` `Mathlib.AlgebraicGeometry.GluingOneHypercover` `Mathlib.AlgebraicGeometry.Gluing` `Mathlib.AlgebraicGeometry.Group.Abelian` `Mathlib.AlgebraicGeometry.Group.Smooth` `Mathlib.AlgebraicGeometry.IdealSheaf.Basic` `Mathlib.AlgebraicGeometry.IdealSheaf.Functorial` `Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent` `Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme` `Mathlib.AlgebraicGeometry.LimitsOver` `Mathlib.AlgebraicGeometry.Limits` `Mathlib.AlgebraicGeometry.Modules.Presheaf` `Mathlib.AlgebraicGeometry.Modules.Sheaf` `Mathlib.AlgebraicGeometry.Modules.Tilde` `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.Etale` `Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation` `Mathlib.AlgebraicGeometry.Morphisms.FiniteType` `Mathlib.AlgebraicGeometry.Morphisms.Finite` `Mathlib.AlgebraicGeometry.Morphisms.FlatDescent` `Mathlib.AlgebraicGeometry.Morphisms.FlatMono` `Mathlib.AlgebraicGeometry.Morphisms.Flat` `Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified` `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.QuasiFinite` `Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated` `Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties` `Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant` `Mathlib.AlgebraicGeometry.Morphisms.Separated` `Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber` `Mathlib.AlgebraicGeometry.Morphisms.Smooth` `Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks` `Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap` `Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed` `Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective` `Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen` `Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale` `Mathlib.AlgebraicGeometry.Noetherian` `Mathlib.AlgebraicGeometry.Normalization` `Mathlib.AlgebraicGeometry.OpenImmersion` `Mathlib.AlgebraicGeometry.Over` `Mathlib.AlgebraicGeometry.PointsPi` `Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic` `Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor` `Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper` `Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme` `Mathlib.AlgebraicGeometry.Properties` `Mathlib.AlgebraicGeometry.PullbackCarrier` `Mathlib.AlgebraicGeometry.Pullbacks` `Mathlib.AlgebraicGeometry.QuasiAffine` `Mathlib.AlgebraicGeometry.RationalMap` `Mathlib.AlgebraicGeometry.RelativeGluing` `Mathlib.AlgebraicGeometry.ResidueField` `Mathlib.AlgebraicGeometry.Restrict` `Mathlib.AlgebraicGeometry.Scheme` `Mathlib.AlgebraicGeometry.Sites.BigZariski` `Mathlib.AlgebraicGeometry.Sites.ConstantSheaf` `Mathlib.AlgebraicGeometry.Sites.ElladicCohomology` `Mathlib.AlgebraicGeometry.Sites.Etale` `Mathlib.AlgebraicGeometry.Sites.Fpqc` `Mathlib.AlgebraicGeometry.Sites.MorphismProperty` `Mathlib.AlgebraicGeometry.Sites.Pretopology` `Mathlib.AlgebraicGeometry.Sites.Proetale` `Mathlib.AlgebraicGeometry.Sites.QuasiCompact` `Mathlib.AlgebraicGeometry.Sites.Representability` `Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact` `Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski` `Mathlib.AlgebraicGeometry.Sites.Small` `Mathlib.AlgebraicGeometry.Spec` `Mathlib.AlgebraicGeometry.SpreadingOut` `Mathlib.AlgebraicGeometry.Stalk` `Mathlib.AlgebraicGeometry.StructureSheaf` `Mathlib.AlgebraicGeometry.ValuativeCriterion` `Mathlib.AlgebraicGeometry.ZariskisMainTheorem` `Mathlib.Analysis.AbsoluteValue.Equivalence` `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.IteratedFDeriv` `Mathlib.Analysis.Analytic.Linear` `Mathlib.Analysis.Analytic.OfScalars` `Mathlib.Analysis.Analytic.Order` `Mathlib.Analysis.Analytic.RadiusLiminf` `Mathlib.Analysis.Analytic.Uniqueness` `Mathlib.Analysis.Analytic.WithLp` `Mathlib.Analysis.Analytic.Within` `Mathlib.Analysis.Asymptotics.ExpGrowth` `Mathlib.Analysis.Asymptotics.SpecificAsymptotics` `Mathlib.Analysis.Asymptotics.SuperpolynomialDecay` `Mathlib.Analysis.BoxIntegral.Partition.Additive` `Mathlib.Analysis.CStarAlgebra.ApproximateUnit` `Mathlib.Analysis.CStarAlgebra.CStarMatrix` `Mathlib.Analysis.CStarAlgebra.Classes` `Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Projection` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart` `Mathlib.Analysis.CStarAlgebra.ContinuousMap` `Mathlib.Analysis.CStarAlgebra.Exponential` `Mathlib.Analysis.CStarAlgebra.Fuglede` `Mathlib.Analysis.CStarAlgebra.GelfandDuality` `Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal` `Mathlib.Analysis.CStarAlgebra.Hom` `Mathlib.Analysis.CStarAlgebra.Module.Constructions` `Mathlib.Analysis.CStarAlgebra.Module.Defs` `Mathlib.Analysis.CStarAlgebra.Multiplier` `Mathlib.Analysis.CStarAlgebra.PositiveLinearMap` `Mathlib.Analysis.CStarAlgebra.Projection` `Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart` `Mathlib.Analysis.CStarAlgebra.Spectrum` `Mathlib.Analysis.CStarAlgebra.Unitary.Connected` `Mathlib.Analysis.CStarAlgebra.Unitary.Span` `Mathlib.Analysis.CStarAlgebra.Unitization` `Mathlib.Analysis.CStarAlgebra.lpSpace` `Mathlib.Analysis.Calculus.AddTorsor.AffineMap` `Mathlib.Analysis.Calculus.Conformal.InnerProduct` `Mathlib.Analysis.Calculus.Conformal.NormedSpace` `Mathlib.Analysis.Calculus.ContDiff.Basic` `Mathlib.Analysis.Calculus.ContDiff.Bounds` `Mathlib.Analysis.Calculus.ContDiff.CPolynomial` `Mathlib.Analysis.Calculus.ContDiff.Comp` `Mathlib.Analysis.Calculus.ContDiff.Defs` `Mathlib.Analysis.Calculus.ContDiff.Deriv` `Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries` `Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno` `Mathlib.Analysis.Calculus.ContDiff.Operations` `Mathlib.Analysis.Calculus.ContDiff.RCLike` `Mathlib.Analysis.Calculus.ContDiff.RestrictScalars` `Mathlib.Analysis.Calculus.ContDiff.WithLp` `Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise` `Mathlib.Analysis.Calculus.DSlope` `Mathlib.Analysis.Calculus.Darboux` `Mathlib.Analysis.Calculus.Deriv.Add` `Mathlib.Analysis.Calculus.Deriv.AffineMap` `Mathlib.Analysis.Calculus.Deriv.Basic` `Mathlib.Analysis.Calculus.Deriv.CompMul` `Mathlib.Analysis.Calculus.Deriv.Comp` `Mathlib.Analysis.Calculus.Deriv.Inv` `Mathlib.Analysis.Calculus.Deriv.Inverse` `Mathlib.Analysis.Calculus.Deriv.Linear` `Mathlib.Analysis.Calculus.Deriv.MeanValue` `Mathlib.Analysis.Calculus.Deriv.Mul` `Mathlib.Analysis.Calculus.Deriv.Pi` `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.Support` `Mathlib.Analysis.Calculus.Deriv.ZPow` `Mathlib.Analysis.Calculus.DerivativeTest` `Mathlib.Analysis.Calculus.DiffContOnCl` `Mathlib.Analysis.Calculus.DifferentialForm.Basic` `Mathlib.Analysis.Calculus.DifferentialForm.VectorField` `Mathlib.Analysis.Calculus.FDeriv.Add` `Mathlib.Analysis.Calculus.FDeriv.Affine` `Mathlib.Analysis.Calculus.FDeriv.Analytic` `Mathlib.Analysis.Calculus.FDeriv.Basic` `Mathlib.Analysis.Calculus.FDeriv.Bilinear` `Mathlib.Analysis.Calculus.FDeriv.CompCLM` `Mathlib.Analysis.Calculus.FDeriv.Comp` `Mathlib.Analysis.Calculus.FDeriv.Congr` `Mathlib.Analysis.Calculus.FDeriv.Const` `Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap` `Mathlib.Analysis.Calculus.FDeriv.ContinuousMultilinearMap` `Mathlib.Analysis.Calculus.FDeriv.Equiv` `Mathlib.Analysis.Calculus.FDeriv.Extend` `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.RestrictScalars` `Mathlib.Analysis.Calculus.FDeriv.Star` `Mathlib.Analysis.Calculus.FDeriv.Symmetric` `Mathlib.Analysis.Calculus.FDeriv.WithLp` `Mathlib.Analysis.Calculus.FormalMultilinearSeries` `Mathlib.Analysis.Calculus.InverseFunctionTheorem.Analytic` `Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn` `Mathlib.Analysis.Calculus.InverseFunctionTheorem.ContDiff` `Mathlib.Analysis.Calculus.InverseFunctionTheorem.Deriv` `Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv` `Mathlib.Analysis.Calculus.IteratedDeriv.ConvergenceOnBall` `Mathlib.Analysis.Calculus.IteratedDeriv.Defs` `Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno` `Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas` `Mathlib.Analysis.Calculus.IteratedDeriv.WithinZpow` `Mathlib.Analysis.Calculus.LHopital` `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.Calculus.LogDeriv` `Mathlib.Analysis.Calculus.MeanValue` `Mathlib.Analysis.Calculus.SmoothSeries` `Mathlib.Analysis.Calculus.TangentCone.Seq` `Mathlib.Analysis.Calculus.UniformLimitsDeriv` `Mathlib.Analysis.Calculus.VectorField` `Mathlib.Analysis.Complex.AbelLimit` `Mathlib.Analysis.Complex.Angle` `Mathlib.Analysis.Complex.Arg` `Mathlib.Analysis.Complex.Asymptotics` `Mathlib.Analysis.Complex.Basic` `Mathlib.Analysis.Complex.CanonicalDecomposition` `Mathlib.Analysis.Complex.Circle` `Mathlib.Analysis.Complex.Convex` `Mathlib.Analysis.Complex.ExponentialBounds` `Mathlib.Analysis.Complex.HalfPlane` `Mathlib.Analysis.Complex.IntegerCompl` `Mathlib.Analysis.Complex.OpenMapping` `Mathlib.Analysis.Complex.Polynomial.Basic` `Mathlib.Analysis.Complex.Polynomial.GaussLucas` `Mathlib.Analysis.Complex.Polynomial.UnitTrinomial` `Mathlib.Analysis.Complex.ReImTopology` `Mathlib.Analysis.Complex.RealDeriv` `Mathlib.Analysis.Complex.Spectrum` `Mathlib.Analysis.Complex.SqrtDeriv` `Mathlib.Analysis.Complex.UnitDisc.Basic` `Mathlib.Analysis.Complex.UpperHalfPlane.Basic` `Mathlib.Analysis.Complex.UpperHalfPlane.Manifold` `Mathlib.Analysis.Complex.UpperHalfPlane.Measure` `Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction` `Mathlib.Analysis.Convex.AmpleSet` `Mathlib.Analysis.Convex.Deriv` `Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion` `Mathlib.Analysis.Convex.SpecificFunctions.Basic` `Mathlib.Analysis.Convex.SpecificFunctions.Deriv` `Mathlib.Analysis.Convex.SpecificFunctions.Pow` `Mathlib.Analysis.Convex.Strong` `Mathlib.Analysis.Distribution.ContDiffMapSupportedIn` `Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality` `Mathlib.Analysis.Fourier.ZMod` `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.JointEigenspace` `Mathlib.Analysis.InnerProductSpace.LinearMap` `Mathlib.Analysis.InnerProductSpace.OfNorm` `Mathlib.Analysis.InnerProductSpace.Orthogonal` `Mathlib.Analysis.InnerProductSpace.Orthonormal` `Mathlib.Analysis.InnerProductSpace.Positive` `Mathlib.Analysis.InnerProductSpace.Projection.Minimal` `Mathlib.Analysis.InnerProductSpace.Rayleigh` `Mathlib.Analysis.InnerProductSpace.Reproducing` `Mathlib.Analysis.InnerProductSpace.Semisimple` `Mathlib.Analysis.InnerProductSpace.SingularValues` `Mathlib.Analysis.InnerProductSpace.Spectrum` `Mathlib.Analysis.InnerProductSpace.StandardSubspace` `Mathlib.Analysis.InnerProductSpace.StarOrder` `Mathlib.Analysis.InnerProductSpace.Subspace` `Mathlib.Analysis.InnerProductSpace.Symmetric` `Mathlib.Analysis.InnerProductSpace.Trace` `Mathlib.Analysis.LocallyConvex.ContinuousOfBounded` `Mathlib.Analysis.LocallyConvex.PointwiseConvergence` `Mathlib.Analysis.LocallyConvex.StrongTopology` `Mathlib.Analysis.Matrix.HermitianFunctionalCalculus` `Mathlib.Analysis.Matrix.LDL` `Mathlib.Analysis.Matrix.Order` `Mathlib.Analysis.Matrix.PosDef` `Mathlib.Analysis.Matrix.Spectrum` `Mathlib.Analysis.MeanInequalitiesPow` `Mathlib.Analysis.MeanInequalities` `Mathlib.Analysis.Meromorphic.Basic` `Mathlib.Analysis.Meromorphic.Divisor` `Mathlib.Analysis.Meromorphic.FactorizedRational` `Mathlib.Analysis.Meromorphic.IsolatedZeros` `Mathlib.Analysis.Meromorphic.NormalForm` `Mathlib.Analysis.Meromorphic.Order` `Mathlib.Analysis.Meromorphic.TrailingCoefficient` `Mathlib.Analysis.Normed.Affine.ContinuousAffineMap` `Mathlib.Analysis.Normed.Algebra.Basic` `Mathlib.Analysis.Normed.Algebra.DualNumber` `Mathlib.Analysis.Normed.Algebra.Exponential` `Mathlib.Analysis.Normed.Algebra.GelfandFormula` `Mathlib.Analysis.Normed.Algebra.GelfandMazur` `Mathlib.Analysis.Normed.Algebra.Spectrum` `Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt` `Mathlib.Analysis.Normed.Algebra.UnitizationL1` `Mathlib.Analysis.Normed.Algebra.Unitization` `Mathlib.Analysis.Normed.Field.Dense` `Mathlib.Analysis.Normed.Field.Krasner` `Mathlib.Analysis.Normed.Field.WithAbs` `Mathlib.Analysis.Normed.Group.ControlledClosure` `Mathlib.Analysis.Normed.Group.ZeroAtInfty` `Mathlib.Analysis.Normed.Lp.LpEquiv` `Mathlib.Analysis.Normed.Lp.MeasurableSpace` `Mathlib.Analysis.Normed.Lp.PiLp` `Mathlib.Analysis.Normed.Lp.ProdLp` `Mathlib.Analysis.Normed.Lp.lpSpace` `Mathlib.Analysis.Normed.Module.Alternating.Basic` `Mathlib.Analysis.Normed.Module.Alternating.Curry` `Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin` `Mathlib.Analysis.Normed.Module.Completion` `Mathlib.Analysis.Normed.Module.Connected` `Mathlib.Analysis.Normed.Module.Multilinear.Basic` `Mathlib.Analysis.Normed.Module.Multilinear.Curry` `Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm` `Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm` `Mathlib.Analysis.Normed.Module.RCLike.Basic` `Mathlib.Analysis.Normed.Module.RCLike.Extend` `Mathlib.Analysis.Normed.Module.RieszLemma` `Mathlib.Analysis.Normed.Operator.Asymptotics` `Mathlib.Analysis.Normed.Operator.BanachSteinhaus` `Mathlib.Analysis.Normed.Operator.Banach` `Mathlib.Analysis.Normed.Operator.Basic` `Mathlib.Analysis.Normed.Operator.Bilinear` `Mathlib.Analysis.Normed.Operator.BoundedLinearMaps` `Mathlib.Analysis.Normed.Operator.Compact` `Mathlib.Analysis.Normed.Operator.Completeness` `Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv` `Mathlib.Analysis.Normed.Operator.Extend` `Mathlib.Analysis.Normed.Operator.FredholmAlternative` `Mathlib.Analysis.Normed.Operator.Mul` `Mathlib.Analysis.Normed.Operator.NNNorm` `Mathlib.Analysis.Normed.Operator.NormedSpace` `Mathlib.Analysis.Normed.Operator.Prod` `Mathlib.Analysis.Normed.Ring.Units` `Mathlib.Analysis.Normed.Unbundled.AlgebraNorm` `Mathlib.Analysis.Normed.Unbundled.FiniteExtension` `Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful` `Mathlib.Analysis.Normed.Unbundled.RingSeminorm` `Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded` `Mathlib.Analysis.Normed.Unbundled.SeminormFromConst` `Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm` `Mathlib.Analysis.Normed.Unbundled.SpectralNorm` `Mathlib.Analysis.ODE.Basic` `Mathlib.Analysis.ODE.Gronwall` `Mathlib.Analysis.ODE.Transform` `Mathlib.Analysis.PSeries` `Mathlib.Analysis.Polynomial.CauchyBound` `Mathlib.Analysis.Polynomial.Factorization` `Mathlib.Analysis.Polynomial.MahlerMeasure` `Mathlib.Analysis.RCLike.BoundedContinuous` `Mathlib.Analysis.RCLike.Sqrt` `Mathlib.Analysis.Real.Hyperreal` `Mathlib.Analysis.Real.OfDigits` `Mathlib.Analysis.Real.Pi.Bounds` `Mathlib.Analysis.SpecialFunctions.Arcosh` `Mathlib.Analysis.SpecialFunctions.Arsinh` `Mathlib.Analysis.SpecialFunctions.Artanh` `Mathlib.Analysis.SpecialFunctions.BinaryEntropy` `Mathlib.Analysis.SpecialFunctions.CompareExp` `Mathlib.Analysis.SpecialFunctions.Complex.Arg` `Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar` `Mathlib.Analysis.SpecialFunctions.Complex.CircleMap` `Mathlib.Analysis.SpecialFunctions.Complex.Circle` `Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv` `Mathlib.Analysis.SpecialFunctions.Complex.Log` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Isometric` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.ConjSqrt` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder` `Mathlib.Analysis.SpecialFunctions.ExpDeriv` `Mathlib.Analysis.SpecialFunctions.Exp` `Mathlib.Analysis.SpecialFunctions.Exponential` `Mathlib.Analysis.SpecialFunctions.Log.Base` `Mathlib.Analysis.SpecialFunctions.Log.Basic` `Mathlib.Analysis.SpecialFunctions.Log.Deriv` `Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp` `Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog` `Mathlib.Analysis.SpecialFunctions.Log.InvLog` `Mathlib.Analysis.SpecialFunctions.Log.Monotone` `Mathlib.Analysis.SpecialFunctions.Log.NegMulLog` `Mathlib.Analysis.SpecialFunctions.Log.PosLog` `Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto` `Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq` `Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric` `Mathlib.Analysis.SpecialFunctions.Pochhammer` `Mathlib.Analysis.SpecialFunctions.PolynomialExp` `Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics` `Mathlib.Analysis.SpecialFunctions.Pow.Complex` `Mathlib.Analysis.SpecialFunctions.Pow.Continuity` `Mathlib.Analysis.SpecialFunctions.Pow.Deriv` `Mathlib.Analysis.SpecialFunctions.Pow.NNReal` `Mathlib.Analysis.SpecialFunctions.Pow.Real` `Mathlib.Analysis.SpecialFunctions.Sigmoid` `Mathlib.Analysis.SpecialFunctions.Sqrt` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle` `Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema` `Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex` `Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv` `Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Series` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc` `Mathlib.Analysis.SpecificLimits.FloorPow` `Mathlib.Analysis.SpecificLimits.Normed` `Mathlib.CategoryTheory.Preadditive.HomOrthogonal` `Mathlib.CategoryTheory.Preadditive.Schur` `Mathlib.Combinatorics.Additive.Corner.Roth` `Mathlib.Combinatorics.Additive.ErdosGinzburgZiv` `Mathlib.Combinatorics.Derangements.Exponential` `Mathlib.Combinatorics.SimpleGraph.LapMatrix` `Mathlib.Combinatorics.SimpleGraph.Regularity.Bound` `Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk` `Mathlib.Combinatorics.SimpleGraph.Regularity.Increment` `Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma` `Mathlib.Combinatorics.SimpleGraph.Triangle.Removal` `Mathlib.Computability.AkraBazzi.AkraBazzi` `Mathlib.Computability.AkraBazzi.GrowsPolynomially` `Mathlib.Computability.AkraBazzi.SumTransform` `Mathlib.Computability.TMComputable` `Mathlib.Computability.TuringMachine.Computable` `Mathlib.Data.Nat.Choose.Vandermonde` `Mathlib.Data.ZMod.QuotientRing` `Mathlib.Dynamics.TopologicalEntropy.CoverEntropy` `Mathlib.Dynamics.TopologicalEntropy.NetEntropy` `Mathlib.Dynamics.TopologicalEntropy.Semiconj` `Mathlib.Dynamics.TopologicalEntropy.Subset` `Mathlib.FieldTheory.AbelRuffini` `Mathlib.FieldTheory.AbsoluteGaloisGroup` `Mathlib.FieldTheory.AlgebraicClosure` `Mathlib.FieldTheory.AxGrothendieck` `Mathlib.FieldTheory.CardinalEmb` `Mathlib.FieldTheory.Cardinality` `Mathlib.FieldTheory.ChevalleyWarning` `Mathlib.FieldTheory.Differential.Basic` `Mathlib.FieldTheory.Differential.Liouville` `Mathlib.FieldTheory.Extension` `Mathlib.FieldTheory.Finite.Basic` `Mathlib.FieldTheory.Finite.Extension` `Mathlib.FieldTheory.Finite.GaloisField` `Mathlib.FieldTheory.Finite.Polynomial` `Mathlib.FieldTheory.Finite.Trace` `Mathlib.FieldTheory.Finite.Valuation` `Mathlib.FieldTheory.Finiteness` `Mathlib.FieldTheory.Fixed` `Mathlib.FieldTheory.Galois.Abelian` `Mathlib.FieldTheory.Galois.Basic` `Mathlib.FieldTheory.Galois.GaloisClosure` `Mathlib.FieldTheory.Galois.Infinite` `Mathlib.FieldTheory.Galois.IsGaloisGroup` `Mathlib.FieldTheory.Galois.NormalBasis` `Mathlib.FieldTheory.Galois.Profinite` `Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra` `Mathlib.FieldTheory.IntermediateField.Adjoin.Basic` `Mathlib.FieldTheory.IntermediateField.Algebraic` `Mathlib.FieldTheory.IntermediateField.ExtendRight` `Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure` `Mathlib.FieldTheory.IsAlgClosed.Basic` `Mathlib.FieldTheory.IsAlgClosed.Classification` `Mathlib.FieldTheory.IsAlgClosed.Spectrum` `Mathlib.FieldTheory.IsPerfectClosure` `Mathlib.FieldTheory.IsRealClosed.Basic` `Mathlib.FieldTheory.IsSepClosed` `Mathlib.FieldTheory.Isaacs` `Mathlib.FieldTheory.JacobsonNoether` `Mathlib.FieldTheory.KrullTopology` `Mathlib.FieldTheory.KummerExtension` `Mathlib.FieldTheory.KummerPolynomial` `Mathlib.FieldTheory.Laurent` `Mathlib.FieldTheory.LinearDisjoint` `Mathlib.FieldTheory.Minpoly.ConjRootClass` `Mathlib.FieldTheory.Minpoly.Field` `Mathlib.FieldTheory.Minpoly.IsConjRoot` `Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed` `Mathlib.FieldTheory.Minpoly.MinpolyDiv` `Mathlib.FieldTheory.Normal.Basic` `Mathlib.FieldTheory.Normal.Closure` `Mathlib.FieldTheory.Normal.Defs` `Mathlib.FieldTheory.NormalizedTrace` `Mathlib.FieldTheory.PerfectClosure` `Mathlib.FieldTheory.Perfect` `Mathlib.FieldTheory.PolynomialGaloisGroup` `Mathlib.FieldTheory.PrimitiveElement` `Mathlib.FieldTheory.PurelyInseparable.Basic` `Mathlib.FieldTheory.PurelyInseparable.Exponent` `Mathlib.FieldTheory.PurelyInseparable.PerfectClosure` `Mathlib.FieldTheory.PurelyInseparable.Tower` `Mathlib.FieldTheory.RatFunc.AsPolynomial` `Mathlib.FieldTheory.RatFunc.Basic` `Mathlib.FieldTheory.RatFunc.Defs` `Mathlib.FieldTheory.RatFunc.Degree` `Mathlib.FieldTheory.RatFunc.IntermediateField` `Mathlib.FieldTheory.RatFunc.Luroth` `Mathlib.FieldTheory.Relrank` `Mathlib.FieldTheory.SeparableClosure` `Mathlib.FieldTheory.SeparableDegree` `Mathlib.FieldTheory.Separable` `Mathlib.FieldTheory.SeparablyGenerated` `Mathlib.FieldTheory.SplittingField.Construction` `Mathlib.FieldTheory.SplittingField.IsSplittingField` `Mathlib.FieldTheory.Tower` `Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic` `Mathlib.Geometry.Euclidean.Angle.Unoriented.Conformal` `Mathlib.Geometry.Euclidean.Inversion.Basic` `Mathlib.Geometry.Manifold.ConformalGroupoid` `Mathlib.Geometry.Manifold.IsManifold.Basic` `Mathlib.Geometry.Manifold.LocalSourceTargetProperty` `Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField` `Mathlib.GroupTheory.FiniteAbelian.Basic` `Mathlib.GroupTheory.FiniteAbelian.Duality` `Mathlib.GroupTheory.FreeGroup.GeneratorEquiv` `Mathlib.GroupTheory.SpecificGroups.ZGroup` `Mathlib.InformationTheory.Coding.KraftMcMillan` `Mathlib.LinearAlgebra.AnnihilatingPolynomial` `Mathlib.LinearAlgebra.Basis.MulOpposite` `Mathlib.LinearAlgebra.Center` `Mathlib.LinearAlgebra.Charpoly.BaseChange` `Mathlib.LinearAlgebra.Charpoly.Basic` `Mathlib.LinearAlgebra.Charpoly.ToMatrix` `Mathlib.LinearAlgebra.Complex.FiniteDimensional` `Mathlib.LinearAlgebra.Complex.Module` `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.Dimension.Torsion.Basic` `Mathlib.LinearAlgebra.Dimension.Torsion.Finite` `Mathlib.LinearAlgebra.DirectSum.Basis` `Mathlib.LinearAlgebra.Eigenspace.Basic` `Mathlib.LinearAlgebra.Eigenspace.Charpoly` `Mathlib.LinearAlgebra.Eigenspace.ContinuousLinearMap` `Mathlib.LinearAlgebra.Eigenspace.Matrix` `Mathlib.LinearAlgebra.Eigenspace.Pi` `Mathlib.LinearAlgebra.Eigenspace.Semisimple` `Mathlib.LinearAlgebra.Eigenspace.Triangularizable` `Mathlib.LinearAlgebra.Eigenspace.Zero` `Mathlib.LinearAlgebra.FiniteDimensional.Basic` `Mathlib.LinearAlgebra.FiniteDimensional.Defs` `Mathlib.LinearAlgebra.FiniteDimensional.Lemmas` `Mathlib.LinearAlgebra.Finsupp.VectorSpace` `Mathlib.LinearAlgebra.FreeModule.Finite.Basic` `Mathlib.LinearAlgebra.FreeModule.Int` `Mathlib.LinearAlgebra.FreeModule.ModN` `Mathlib.LinearAlgebra.FreeModule.Norm` `Mathlib.LinearAlgebra.FreeModule.PID` `Mathlib.LinearAlgebra.InvariantBasisNumber` `Mathlib.LinearAlgebra.JordanChevalley` `Mathlib.LinearAlgebra.LinearIndependent.BaseChange` `Mathlib.LinearAlgebra.Matrix.Basis` `Mathlib.LinearAlgebra.Matrix.Charpoly.Disc` `Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs` `Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField` `Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly` `Mathlib.LinearAlgebra.Matrix.Diagonal` `Mathlib.LinearAlgebra.Matrix.Dual` `Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo` `Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber` `Mathlib.LinearAlgebra.Matrix.LDL` `Mathlib.LinearAlgebra.Matrix.Polynomial` `Mathlib.LinearAlgebra.Matrix.StdBasis` `Mathlib.LinearAlgebra.Matrix.ToLin` `Mathlib.LinearAlgebra.Matrix.WithConv` `Mathlib.LinearAlgebra.PiTensorProduct.Basis` `Mathlib.LinearAlgebra.PiTensorProduct.Dual` `Mathlib.LinearAlgebra.Projectivization.Action` `Mathlib.LinearAlgebra.Projectivization.Basic` `Mathlib.LinearAlgebra.Projectivization.Cardinality` `Mathlib.LinearAlgebra.Projectivization.Constructions` `Mathlib.LinearAlgebra.Projectivization.Independence` `Mathlib.LinearAlgebra.Projectivization.Subspace` `Mathlib.LinearAlgebra.QuadraticForm.AlgClosed` `Mathlib.LinearAlgebra.QuadraticForm.Complex` `Mathlib.LinearAlgebra.RootSystem.BaseChange` `Mathlib.LinearAlgebra.RootSystem.BaseExists` `Mathlib.LinearAlgebra.RootSystem.Base` `Mathlib.LinearAlgebra.RootSystem.Basic` `Mathlib.LinearAlgebra.RootSystem.CartanMatrix` `Mathlib.LinearAlgebra.RootSystem.Chain` `Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear` `Mathlib.LinearAlgebra.RootSystem.Finite.G2` `Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas` `Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate` `Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic` `Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis` `Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas` `Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations` `Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple` `Mathlib.LinearAlgebra.RootSystem.Hom` `Mathlib.LinearAlgebra.RootSystem.Irreducible` `Mathlib.LinearAlgebra.RootSystem.IsValuedIn` `Mathlib.LinearAlgebra.RootSystem.Reduced` `Mathlib.LinearAlgebra.RootSystem.RootPairingCat` `Mathlib.LinearAlgebra.RootSystem.RootPositive` `Mathlib.LinearAlgebra.RootSystem.WeylGroup` `Mathlib.LinearAlgebra.SModEq.Basic` `Mathlib.LinearAlgebra.SModEq.Pointwise` `Mathlib.LinearAlgebra.SModEq.Pow` `Mathlib.LinearAlgebra.SModEq` `Mathlib.LinearAlgebra.Semisimple` `Mathlib.LinearAlgebra.SpecialLinearGroup` `Mathlib.LinearAlgebra.StdBasis` `Mathlib.LinearAlgebra.TensorProduct.Basis` `Mathlib.LinearAlgebra.TensorProduct.Matrix` `Mathlib.LinearAlgebra.Transvection.Basic` `Mathlib.LinearAlgebra.Transvection` `Mathlib.MeasureTheory.Constructions.BorelSpace.Complex` `Mathlib.MeasureTheory.Function.ConvergenceInMeasure` `Mathlib.MeasureTheory.Function.LpOrder` `Mathlib.MeasureTheory.Function.LpSeminorm.Basic` `Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov` `Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp` `Mathlib.MeasureTheory.Function.LpSeminorm.Count` `Mathlib.MeasureTheory.Function.LpSeminorm.Defs` `Mathlib.MeasureTheory.Function.LpSeminorm.Indicator` `Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity` `Mathlib.MeasureTheory.Function.LpSeminorm.Prod` `Mathlib.MeasureTheory.Function.LpSeminorm.SMul` `Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality` `Mathlib.MeasureTheory.Function.LpSeminorm.Trim` `Mathlib.MeasureTheory.Function.LpSpace.Basic` `Mathlib.MeasureTheory.Function.LpSpace.Complete` `Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions` `Mathlib.MeasureTheory.Function.LpSpace.Indicator` `Mathlib.MeasureTheory.Function.SpecialFunctions.Arctan` `Mathlib.MeasureTheory.Function.SpecialFunctions.Basic` `Mathlib.MeasureTheory.Function.SpecialFunctions.Inner` `Mathlib.MeasureTheory.Function.StronglyMeasurable.Inner` `Mathlib.MeasureTheory.Integral.MeanInequalities` `Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic` `Mathlib.MeasureTheory.Measure.Complex` `Mathlib.ModelTheory.Algebra.Field.IsAlgClosed` `Mathlib.ModelTheory.Algebra.Ring.Definability` `Mathlib.ModelTheory.Arithmetic.Presburger.Definability` `Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic` `Mathlib.NumberTheory.ArithmeticFunction.Carmichael` `Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt` `Mathlib.NumberTheory.ArithmeticFunction` `Mathlib.NumberTheory.Bertrand` `Mathlib.NumberTheory.ClassNumber.Finite` `Mathlib.NumberTheory.ClassNumber.FunctionField` `Mathlib.NumberTheory.Cyclotomic.Basic` `Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter` `Mathlib.NumberTheory.Cyclotomic.Discriminant` `Mathlib.NumberTheory.Cyclotomic.Gal` `Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots` `Mathlib.NumberTheory.DirichletCharacter.Bounds` `Mathlib.NumberTheory.DirichletCharacter.GaussSum` `Mathlib.NumberTheory.DirichletCharacter.Orthogonality` `Mathlib.NumberTheory.EulerProduct.Basic` `Mathlib.NumberTheory.EulerProduct.DirichletLSeries` `Mathlib.NumberTheory.FLT.Three` `Mathlib.NumberTheory.FermatPsp` `Mathlib.NumberTheory.Fermat` `Mathlib.NumberTheory.FrobeniusNumber` `Mathlib.NumberTheory.FunctionField` `Mathlib.NumberTheory.GaussSum` `Mathlib.NumberTheory.Harmonic.EulerMascheroni` `Mathlib.NumberTheory.Height.Basic` `Mathlib.NumberTheory.Height.NumberField` `Mathlib.NumberTheory.Height.Projectivization` `Mathlib.NumberTheory.JacobiSum.Basic` `Mathlib.NumberTheory.KummerDedekind` `Mathlib.NumberTheory.LSeries.DirichletContinuation` `Mathlib.NumberTheory.LSeries.Dirichlet` `Mathlib.NumberTheory.LSeries.Nonvanishing` `Mathlib.NumberTheory.LSeries.PrimesInAP` `Mathlib.NumberTheory.LSeries.ZMod` `Mathlib.NumberTheory.LSeries.ZetaZeros` `Mathlib.NumberTheory.LegendreSymbol.AddCharacter` `Mathlib.NumberTheory.LegendreSymbol.Basic` `Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas` `Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol` `Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic` `Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum` `Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity` `Mathlib.NumberTheory.LocalField.Basic` `Mathlib.NumberTheory.LucasLehmer` `Mathlib.NumberTheory.MahlerMeasure` `Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups` `Mathlib.NumberTheory.ModularForms.Basic` `Mathlib.NumberTheory.ModularForms.BoundedAtCusp` `Mathlib.NumberTheory.ModularForms.Bounds` `Mathlib.NumberTheory.ModularForms.CongruenceSubgroups` `Mathlib.NumberTheory.ModularForms.Cusps` `Mathlib.NumberTheory.ModularForms.DedekindEta` `Mathlib.NumberTheory.ModularForms.Delta` `Mathlib.NumberTheory.ModularForms.Derivative` `Mathlib.NumberTheory.ModularForms.Discriminant` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.MDifferentiable` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence` `Mathlib.NumberTheory.ModularForms.Identities` `Mathlib.NumberTheory.ModularForms.JacobiTheta.Manifold` `Mathlib.NumberTheory.ModularForms.LevelOne` `Mathlib.NumberTheory.ModularForms.NormTrace` `Mathlib.NumberTheory.ModularForms.Petersson` `Mathlib.NumberTheory.ModularForms.QExpansion` `Mathlib.NumberTheory.ModularForms.SlashInvariantForms` `Mathlib.NumberTheory.MulChar.Duality` `Mathlib.NumberTheory.Niven` `Mathlib.NumberTheory.NumberField.AdeleRing` `Mathlib.NumberTheory.NumberField.Basic` `Mathlib.NumberTheory.NumberField.CMField` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord` `Mathlib.NumberTheory.NumberField.ClassNumber` `Mathlib.NumberTheory.NumberField.Completion.FinitePlace` `Mathlib.NumberTheory.NumberField.Completion.InfinitePlace` `Mathlib.NumberTheory.NumberField.Completion.LiesOverInstances` `Mathlib.NumberTheory.NumberField.Completion.Ramification` `Mathlib.NumberTheory.NumberField.Cyclotomic.Basic` `Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings` `Mathlib.NumberTheory.NumberField.Cyclotomic.Galois` `Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal` `Mathlib.NumberTheory.NumberField.Cyclotomic.PID` `Mathlib.NumberTheory.NumberField.Cyclotomic.Three` `Mathlib.NumberTheory.NumberField.DedekindZeta` `Mathlib.NumberTheory.NumberField.Discriminant.Basic` `Mathlib.NumberTheory.NumberField.Discriminant.Defs` `Mathlib.NumberTheory.NumberField.Discriminant.Different` `Mathlib.NumberTheory.NumberField.EquivReindex` `Mathlib.NumberTheory.NumberField.FinitePlaces` `Mathlib.NumberTheory.NumberField.FractionalIdeal` `Mathlib.NumberTheory.NumberField.House` `Mathlib.NumberTheory.NumberField.Ideal.Asymptotics` `Mathlib.NumberTheory.NumberField.Ideal.Basic` `Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind` `Mathlib.NumberTheory.NumberField.InfiniteAdeleRing` `Mathlib.NumberTheory.NumberField.InfinitePlace.Basic` `Mathlib.NumberTheory.NumberField.InfinitePlace.Completion` `Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings` `Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification` `Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex` `Mathlib.NumberTheory.NumberField.Norm` `Mathlib.NumberTheory.NumberField.ProductFormula` `Mathlib.NumberTheory.NumberField.Units.Basic` `Mathlib.NumberTheory.NumberField.Units.DirichletTheorem` `Mathlib.NumberTheory.NumberField.Units.Regulator` `Mathlib.NumberTheory.Ostrowski` `Mathlib.NumberTheory.Padics.Complex` `Mathlib.NumberTheory.Padics.HeightOneSpectrum` `Mathlib.NumberTheory.Padics.PadicIntegers` `Mathlib.NumberTheory.Padics.ProperSpace` `Mathlib.NumberTheory.Padics.RingHoms` `Mathlib.NumberTheory.Padics.ValuativeRel` `Mathlib.NumberTheory.Padics.WithVal` `Mathlib.NumberTheory.PowModTotient` `Mathlib.NumberTheory.PrimesCongruentOne` `Mathlib.NumberTheory.RamificationInertia.Basic` `Mathlib.NumberTheory.RamificationInertia.Galois` `Mathlib.NumberTheory.RamificationInertia.HilbertTheory` `Mathlib.NumberTheory.RamificationInertia.Inertia` `Mathlib.NumberTheory.RamificationInertia.Ramification` `Mathlib.NumberTheory.RamificationInertia.Unramified` `Mathlib.NumberTheory.RatFunc.Ostrowski` `Mathlib.NumberTheory.SumFourSquares` `Mathlib.NumberTheory.SumPrimeReciprocals` `Mathlib.NumberTheory.SumTwoSquares` `Mathlib.NumberTheory.TsumDivisorsAntidiagonal` `Mathlib.NumberTheory.VonMangoldt` `Mathlib.NumberTheory.Wilson` `Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity` `Mathlib.Probability.Distributions.Gaussian.CharFun` `Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence` `Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence` `Mathlib.Probability.Distributions.Gaussian.Multivariate` `Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess` `Mathlib.Probability.Moments.CovarianceBilin` `Mathlib.Probability.Process.Kolmogorov` `Mathlib.RepresentationTheory.AlgebraRepresentation.Basic` `Mathlib.RepresentationTheory.Character` `Mathlib.RepresentationTheory.FDRep` `Mathlib.RepresentationTheory.FinGroupCharZero` `Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic` `Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality` `Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90` `Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence` `Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree` `Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic` `Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality` `Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence` `Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree` `Mathlib.RepresentationTheory.Invariants` `Mathlib.RepresentationTheory.Irreducible` `Mathlib.RepresentationTheory.Tannaka` `Mathlib.RingTheory.AdicCompletion.Algebra` `Mathlib.RingTheory.AdicCompletion.Basic` `Mathlib.RingTheory.AdicCompletion.Functoriality` `Mathlib.RingTheory.AdicCompletion.LocalRing` `Mathlib.RingTheory.AdicCompletion.Noetherian` `Mathlib.RingTheory.AdicCompletion.RingHom` `Mathlib.RingTheory.AdicCompletion.Topology` `Mathlib.RingTheory.Adjoin.Dimension` `Mathlib.RingTheory.Adjoin.Field` `Mathlib.RingTheory.Adjoin.Polynomial.Bivariate` `Mathlib.RingTheory.Adjoin.PowerBasis` `Mathlib.RingTheory.AdjoinRoot` `Mathlib.RingTheory.Algebraic.Cardinality` `Mathlib.RingTheory.Algebraic.Integral` `Mathlib.RingTheory.Algebraic.StronglyTranscendental` `Mathlib.RingTheory.AlgebraicIndependent.Adjoin` `Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure` `Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality` `Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis` `Mathlib.RingTheory.Artinian.Module` `Mathlib.RingTheory.Artinian.Ring` `Mathlib.RingTheory.ClassGroup` `Mathlib.RingTheory.Conductor` `Mathlib.RingTheory.DedekindDomain.AdicValuation` `Mathlib.RingTheory.DedekindDomain.Basic` `Mathlib.RingTheory.DedekindDomain.Different` `Mathlib.RingTheory.DedekindDomain.Dvr` `Mathlib.RingTheory.DedekindDomain.Factorization` `Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing` `Mathlib.RingTheory.DedekindDomain.GaussLemma` `Mathlib.RingTheory.DedekindDomain.Ideal.Basic` `Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas` `Mathlib.RingTheory.DedekindDomain.Instances` `Mathlib.RingTheory.DedekindDomain.IntegralClosure` `Mathlib.RingTheory.DedekindDomain.LinearDisjoint` `Mathlib.RingTheory.DedekindDomain.PID` `Mathlib.RingTheory.DedekindDomain.SInteger` `Mathlib.RingTheory.DedekindDomain.SelmerGroup` `Mathlib.RingTheory.Derivation.MapCoeffs` `Mathlib.RingTheory.DiscreteValuationRing.Basic` `Mathlib.RingTheory.DiscreteValuationRing.TFAE` `Mathlib.RingTheory.Discriminant` `Mathlib.RingTheory.Etale.Basic` `Mathlib.RingTheory.Etale.Field` `Mathlib.RingTheory.Etale.Kaehler` `Mathlib.RingTheory.Etale.Locus` `Mathlib.RingTheory.Etale.Pi` `Mathlib.RingTheory.Etale.QuasiFinite` `Mathlib.RingTheory.Etale.StandardEtale` `Mathlib.RingTheory.Extension.Cotangent.BaseChange` `Mathlib.RingTheory.Extension.Cotangent.Basic` `Mathlib.RingTheory.Extension.Cotangent.Basis` `Mathlib.RingTheory.Extension.Cotangent.Free` `Mathlib.RingTheory.Extension.Cotangent.LocalizationAway` `Mathlib.RingTheory.Extension.Generators` `Mathlib.RingTheory.Extension.Presentation.Basic` `Mathlib.RingTheory.Extension.Presentation.Core` `Mathlib.RingTheory.Extension.Presentation.Submersive` `Mathlib.RingTheory.FiniteLength` `Mathlib.RingTheory.FiniteStability` `Mathlib.RingTheory.Finiteness.Cardinality` `Mathlib.RingTheory.Finiteness.Cofinite` `Mathlib.RingTheory.Finiteness.Descent` `Mathlib.RingTheory.Finiteness.FinitePresentationLocal` `Mathlib.RingTheory.Finiteness.Finsupp` `Mathlib.RingTheory.Finiteness.Ideal` `Mathlib.RingTheory.Finiteness.ModuleFinitePresentation` `Mathlib.RingTheory.Finiteness.NilpotentKer` `Mathlib.RingTheory.Finiteness.Nilpotent` `Mathlib.RingTheory.Finiteness.Projective` `Mathlib.RingTheory.Flat.FaithfullyFlat.Descent` `Mathlib.RingTheory.Flat.Rank` `Mathlib.RingTheory.Flat.TorsionFree` `Mathlib.RingTheory.FractionalIdeal.Extended` `Mathlib.RingTheory.FractionalIdeal.Norm` `Mathlib.RingTheory.Frobenius` `Mathlib.RingTheory.GradedAlgebra.Noetherian` `Mathlib.RingTheory.Grassmannian` `Mathlib.RingTheory.HopkinsLevitzki` `Mathlib.RingTheory.Ideal.AssociatedPrime.Basic` `Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness` `Mathlib.RingTheory.Ideal.GoingDown` `Mathlib.RingTheory.Ideal.GoingUp` `Mathlib.RingTheory.Ideal.Height` `Mathlib.RingTheory.Ideal.Int` `Mathlib.RingTheory.Ideal.KrullsHeightTheorem` `Mathlib.RingTheory.Ideal.MinimalPrime.Colon` `Mathlib.RingTheory.Ideal.NatInt` `Mathlib.RingTheory.Ideal.Norm.AbsNorm` `Mathlib.RingTheory.Ideal.Norm.RelNorm` `Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients` `Mathlib.RingTheory.Ideal.Quotient.Index` `Mathlib.RingTheory.Ideal.Quotient.Nilpotent` `Mathlib.RingTheory.Ideal.Quotient.Noetherian` `Mathlib.RingTheory.IntegralClosure.Algebra.Defs` `Mathlib.RingTheory.IntegralClosure.GoingDown` `Mathlib.RingTheory.IntegralClosure.IntegralRestrict` `Mathlib.RingTheory.IntegralClosure.IntegrallyClosed` `Mathlib.RingTheory.IntegralClosure.IsIntegral.Defs` `Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic` `Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Defs` `Mathlib.RingTheory.Invariant.Basic` `Mathlib.RingTheory.Invariant.Profinite` `Mathlib.RingTheory.IsAdjoinRoot` `Mathlib.RingTheory.Jacobson.Artinian` `Mathlib.RingTheory.Jacobson.Ring` `Mathlib.RingTheory.Kaehler.JacobiZariski` `Mathlib.RingTheory.KrullDimension.Basic` `Mathlib.RingTheory.KrullDimension.Field` `Mathlib.RingTheory.KrullDimension.LocalRing` `Mathlib.RingTheory.KrullDimension.Module` `Mathlib.RingTheory.KrullDimension.PID` `Mathlib.RingTheory.KrullDimension.Polynomial` `Mathlib.RingTheory.KrullDimension.Regular` `Mathlib.RingTheory.KrullDimension.Zero` `Mathlib.RingTheory.Lasker` `Mathlib.RingTheory.LaurentSeries` `Mathlib.RingTheory.Length` `Mathlib.RingTheory.LittleWedderburn` `Mathlib.RingTheory.LocalProperties.IntegrallyClosed` `Mathlib.RingTheory.LocalProperties.Semilocal` `Mathlib.RingTheory.LocalRing.ResidueField.Basic` `Mathlib.RingTheory.LocalRing.ResidueField.Fiber` `Mathlib.RingTheory.LocalRing.ResidueField.Instances` `Mathlib.RingTheory.LocalRing.ResidueField.Polynomial` `Mathlib.RingTheory.Localization.AtPrime.Extension` `Mathlib.RingTheory.Localization.Away.AdjoinRoot` `Mathlib.RingTheory.Localization.Integral` `Mathlib.RingTheory.Localization.NormTrace` `Mathlib.RingTheory.Localization.Pi` `Mathlib.RingTheory.MvPolynomial.Localization` `Mathlib.RingTheory.Nilpotent.GeometricallyReduced` `Mathlib.RingTheory.Nilpotent.Lemmas` `Mathlib.RingTheory.NoetherNormalization` `Mathlib.RingTheory.Noetherian.Basic` `Mathlib.RingTheory.Noetherian.Nilpotent` `Mathlib.RingTheory.Noetherian.Orzech` `Mathlib.RingTheory.Norm.Basic` `Mathlib.RingTheory.Norm.Transitivity` `Mathlib.RingTheory.NormalClosure` `Mathlib.RingTheory.Nullstellensatz` `Mathlib.RingTheory.OrderOfVanishing` `Mathlib.RingTheory.OrzechProperty` `Mathlib.RingTheory.Perfection` `Mathlib.RingTheory.Perfectoid.BDeRham` `Mathlib.RingTheory.Perfectoid.FontaineTheta` `Mathlib.RingTheory.Perfectoid.Untilt` `Mathlib.RingTheory.PicardGroup` `Mathlib.RingTheory.Polynomial.Cyclotomic.Basic` `Mathlib.RingTheory.Polynomial.Cyclotomic.Eval` `Mathlib.RingTheory.Polynomial.Cyclotomic.Expand` `Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization` `Mathlib.RingTheory.Polynomial.Cyclotomic.Roots` `Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral` `Mathlib.RingTheory.Polynomial.GaussLemma` `Mathlib.RingTheory.Polynomial.Hermite.Basic` `Mathlib.RingTheory.Polynomial.IsIntegral` `Mathlib.RingTheory.Polynomial.Pochhammer` `Mathlib.RingTheory.Polynomial.RationalRoot` `Mathlib.RingTheory.Polynomial.Resultant.Basic` `Mathlib.RingTheory.Polynomial.Selmer` `Mathlib.RingTheory.Polynomial.SeparableDegree` `Mathlib.RingTheory.Polynomial.Subring` `Mathlib.RingTheory.Polynomial.UniversalFactorizationRing` `Mathlib.RingTheory.PowerBasis` `Mathlib.RingTheory.QuasiFinite.Basic` `Mathlib.RingTheory.QuasiFinite.Polynomial` `Mathlib.RingTheory.QuasiFinite.Weakly` `Mathlib.RingTheory.RegularLocalRing.Defs` `Mathlib.RingTheory.RingHom.Etale` `Mathlib.RingTheory.RingHom.FaithfullyFlat` `Mathlib.RingTheory.RingHom.FinitePresentation` `Mathlib.RingTheory.RingHom.FiniteType` `Mathlib.RingTheory.RingHom.Flat` `Mathlib.RingTheory.RingHom.Integral` `Mathlib.RingTheory.RingHom.LocallyStandardSmooth` `Mathlib.RingTheory.RingHom.QuasiFinite` `Mathlib.RingTheory.RingHom.Smooth` `Mathlib.RingTheory.RingHom.StandardSmooth` `Mathlib.RingTheory.RingHom.Unramified` `Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed` `Mathlib.RingTheory.RootsOfUnity.Lemmas` `Mathlib.RingTheory.RootsOfUnity.Minpoly` `Mathlib.RingTheory.SimpleModule.InjectiveProjective` `Mathlib.RingTheory.SimpleModule.IsAlgClosed` `Mathlib.RingTheory.SimpleModule.Rank` `Mathlib.RingTheory.SimpleModule.WedderburnArtin` `Mathlib.RingTheory.Smooth.AdicCompletion` `Mathlib.RingTheory.Smooth.Basic` `Mathlib.RingTheory.Smooth.Fiber` `Mathlib.RingTheory.Smooth.Field` `Mathlib.RingTheory.Smooth.Flat` `Mathlib.RingTheory.Smooth.IntegralClosure` `Mathlib.RingTheory.Smooth.Kaehler` `Mathlib.RingTheory.Smooth.Local` `Mathlib.RingTheory.Smooth.Locus` `Mathlib.RingTheory.Smooth.NoetherianDescent` `Mathlib.RingTheory.Smooth.Pi` `Mathlib.RingTheory.Smooth.Quotient` `Mathlib.RingTheory.Smooth.StandardSmoothCotangent` `Mathlib.RingTheory.Smooth.StandardSmoothOfFree` `Mathlib.RingTheory.Smooth.StandardSmooth` `Mathlib.RingTheory.Spectrum.Maximal.Topology` `Mathlib.RingTheory.Spectrum.Prime.Basic` `Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity` `Mathlib.RingTheory.Spectrum.Prime.Chevalley` `Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet` `Mathlib.RingTheory.Spectrum.Prime.FreeLocus` `Mathlib.RingTheory.Spectrum.Prime.Homeomorph` `Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC` `Mathlib.RingTheory.Spectrum.Prime.Jacobson` `Mathlib.RingTheory.Spectrum.Prime.LTSeries` `Mathlib.RingTheory.Spectrum.Prime.Module` `Mathlib.RingTheory.Spectrum.Prime.Noetherian` `Mathlib.RingTheory.Spectrum.Prime.Polynomial` `Mathlib.RingTheory.Spectrum.Prime.TensorProduct` `Mathlib.RingTheory.Spectrum.Prime.Topology` `Mathlib.RingTheory.Teichmuller` `Mathlib.RingTheory.TensorProduct.Free` `Mathlib.RingTheory.TensorProduct.MvPolynomial` `Mathlib.RingTheory.TotallySplit` `Mathlib.RingTheory.Trace.Basic` `Mathlib.RingTheory.Trace.Quotient` `Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup` `Mathlib.RingTheory.Unramified.Basic` `Mathlib.RingTheory.Unramified.Dedekind` `Mathlib.RingTheory.Unramified.Field` `Mathlib.RingTheory.Unramified.Finite` `Mathlib.RingTheory.Unramified.LocalRing` `Mathlib.RingTheory.Unramified.LocalStructure` `Mathlib.RingTheory.Unramified.Locus` `Mathlib.RingTheory.Unramified.Pi` `Mathlib.RingTheory.Valuation.AlgebraInstances` `Mathlib.RingTheory.Valuation.Discrete.Basic` `Mathlib.RingTheory.Valuation.Discrete.RankOne` `Mathlib.RingTheory.Valuation.DiscreteValuativeRel` `Mathlib.RingTheory.Valuation.Extension` `Mathlib.RingTheory.Valuation.FiniteField` `Mathlib.RingTheory.Valuation.Integral` `Mathlib.RingTheory.Valuation.LocalSubring` `Mathlib.RingTheory.Valuation.Minpoly` `Mathlib.RingTheory.Valuation.RamificationGroup` `Mathlib.RingTheory.Valuation.RankOne` `Mathlib.RingTheory.Valuation.ValuationSubring` `Mathlib.RingTheory.WittVector.Basic` `Mathlib.RingTheory.WittVector.Compare` `Mathlib.RingTheory.WittVector.Complete` `Mathlib.RingTheory.WittVector.Defs` `Mathlib.RingTheory.WittVector.DiscreteValuationRing` `Mathlib.RingTheory.WittVector.Domain` `Mathlib.RingTheory.WittVector.FrobeniusFractionField` `Mathlib.RingTheory.WittVector.Frobenius` `Mathlib.RingTheory.WittVector.Identities` `Mathlib.RingTheory.WittVector.InitTail` `Mathlib.RingTheory.WittVector.IsPoly` `Mathlib.RingTheory.WittVector.Isocrystal` `Mathlib.RingTheory.WittVector.MulCoeff` `Mathlib.RingTheory.WittVector.MulP` `Mathlib.RingTheory.WittVector.StructurePolynomial` `Mathlib.RingTheory.WittVector.TeichmullerSeries` `Mathlib.RingTheory.WittVector.Teichmuller` `Mathlib.RingTheory.WittVector.Truncated` `Mathlib.RingTheory.WittVector.Verschiebung` `Mathlib.RingTheory.ZMod.Torsion` `Mathlib.RingTheory.ZMod.UnitsCyclic` `Mathlib.RingTheory.ZMod` `Mathlib.RingTheory.ZariskisMainTheorem` `Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis` `Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion` `Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized` `Mathlib.Tactic.ComputeDegree` `Mathlib.Tactic.NormNum.LegendreSymbol` `Mathlib.Tactic` `Mathlib.Topology.Algebra.Group.Matrix` `Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn` `Mathlib.Topology.Algebra.Module.Alternating.Topology` `Mathlib.Topology.Algebra.Module.Cardinality` `Mathlib.Topology.Algebra.Module.ModuleTopology` `Mathlib.Topology.Algebra.Module.Multilinear.Topology` `Mathlib.Topology.Algebra.Module.PerfectSpace` `Mathlib.Topology.Algebra.Module.Spaces.CompactConvergenceCLM` `Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap` `Mathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM` `Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM` `Mathlib.Topology.Algebra.Module.StrongTopology` `Mathlib.Topology.Algebra.PontryaginDual` `Mathlib.Topology.Algebra.Ring.Compact` `Mathlib.Topology.Algebra.SeparationQuotient.Section` `Mathlib.Topology.Algebra.Star.LinearMap` `Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology` `Mathlib.Topology.Algebra.Valued.LocallyCompact` `Mathlib.Topology.Algebra.Valued.NormedValued` `Mathlib.Topology.Algebra.Valued.ValuationTopology` `Mathlib.Topology.Algebra.Valued.ValuativeRel` `Mathlib.Topology.Algebra.Valued.ValuedField` `Mathlib.Topology.Algebra.Valued.WithVal` `Mathlib.Topology.Algebra.Valued.WithZeroMulInt` `Mathlib.Topology.Category.Profinite.Nobeling.Induction` `Mathlib.Topology.Compactification.OnePoint.ProjectiveLine` `Mathlib.Topology.ContinuousMap.Bounded.Normed` `Mathlib.Topology.ContinuousMap.Bounded.Star` `Mathlib.Topology.ContinuousMap.BoundedCompactlySupported` `Mathlib.Topology.ContinuousMap.Compact` `Mathlib.Topology.ContinuousMap.CompactlySupported` `Mathlib.Topology.ContinuousMap.ContinuousMapZero` `Mathlib.Topology.ContinuousMap.ContinuousSqrt` `Mathlib.Topology.ContinuousMap.Ideals` `Mathlib.Topology.ContinuousMap.StarOrdered` `Mathlib.Topology.ContinuousMap.Units` `Mathlib.Topology.ContinuousMap.ZeroAtInfty` `Mathlib.Topology.EMetricSpace.PairReduction` `Mathlib.Topology.Instances.CantorSet` `Mathlib.Topology.MetricSpace.GromovHausdorffRealized` `Mathlib.Topology.MetricSpace.GromovHausdorff` `Mathlib.Topology.MetricSpace.HausdorffAlexandroff` `Mathlib.Topology.MetricSpace.HolderNorm` `Mathlib.Topology.MetricSpace.Holder` `Mathlib.Topology.MetricSpace.Kuratowski` `Mathlib.Topology.MetricSpace.Snowflaking` `Mathlib.Topology.MetricSpace.Ultra.ContinuousMaps` `Mathlib.Topology.MetricSpace.UniformConvergence` `Mathlib.Topology.TietzeExtension` `Mathlib.Topology.VectorBundle.Basic` `Mathlib.Topology.VectorBundle.Constructions` `Mathlib.Topology.VectorBundle.FiniteDimensional` `Mathlib.Topology.VectorBundle.Hom` `Mathlib.Topology.VectorBundle.Riemannian`	1
`Mathlib.Algebra.Polynomial.Cardinal`	2

Declarations diff

+ AddMonoidAlgebra
+ _root_.AddMonoidAlgebra.mul'
+ addMonoidHom_ext
+ addSubmonoidClosure_single
+ asAlgebraHom_ofMulAction_smul_eq_mul
+ coeff_add_of_supDegree_le
+ coeff_divOf
+ coeff_domCongr
+ coeff_eq_zero_of_not_le_supDegree
+ coeff_mapAddEquiv
+ coeff_mapAlgHom
+ coeff_mapDomainAddEquiv
+ coeff_mapDomainRingEquiv
+ coeff_mapRingEquiv
+ coeff_mapRingHom
+ coeff_modOf_add_self
+ coeff_modOf_of_exists_add
+ coeff_modOf_of_not_exists_add
+ coeff_modOf_self_add
+ coeff_mul
+ coeff_mul_antidiag
+ coeff_mul_apply_left
+ coeff_mul_apply_right
+ coeff_mul_mul_of_uniqueMul
+ coeff_mul_single_apply
+ coeff_mul_single_eq_coeff_mul
+ coeff_mul_single_mul
+ coeff_mul_single_of_forall_mul_ne
+ coeff_mul_single_one
+ coeff_natCast
+ coeff_ofMulAction
+ coeff_ofNat
+ coeff_of_leftRegular_of_generator
+ coeff_one_one
+ coeff_rTensorAlgEquiv_monomial_tmul
+ coeff_rTensorAlgEquiv_tmul
+ coeff_single
+ coeff_single_apply
+ coeff_single_mul_apply
+ coeff_single_mul_eq_mul_coeff
+ coeff_single_mul_mul
+ coeff_single_mul_of_forall_mul_ne
+ coeff_single_one_mul
+ coeff_smul_apply
+ coeff_supDegree_add_supDegree
+ coeff_toLaurent
+ commRingEquiv_single_one
+ commRingEquiv_single_one_single
+ comul_def
+ curryAddEquiv
+ curryAddEquiv_single
+ curryAddEquiv_symm_single
+ finsuppProd_single
+ induction
+ instAddCommMonoid
+ instInhabited
+ instNontrivial
+ instUnique
+ instance : HMul k[G] (ofMulAction k G G).asModule k[G]
+ instance [DecidableEq R] : DecidableEq R[X] := (toFinsuppIso R).toEquiv.decidableEq
+ instance {σ R : Type*} [CommSemiring R] [Small.{u} R] [Small.{u} σ] :
+ isEmptyAlgEquiv_symm_apply
+ isEmptyAlgEquiv_symm_toRingHom
+ le_inf_support_coeff_add
+ le_inf_support_coeff_finsetProd_le
+ le_inf_support_coeff_mul
+ le_inf_support_coeff_multisetProd
+ mapDomain_smul
+ map_eq_map
+ mem_range_of_mapDomain_ne_zero
+ ofCoeff_single
+ ofNat_def
+ pderiv_sumRingEquiv
+ single_add_erase
+ single_add_single_inj
+ single_inj
+ single_left_inj
+ single_left_injective
+ single_mem_span_single
+ single_right_inj
+ single_right_injective
+ single_sub
+ sumRingEquiv_C
+ sumRingEquiv_X_inl
+ sumRingEquiv_X_inr
+ sumRingEquiv_symm_C_C
+ sumRingEquiv_symm_C_X
+ sumRingEquiv_symm_X
+ sum_coeff_single
+ sup_support_coeff_add_le
+ sup_support_coeff_finsetProd_le
+ sup_support_coeff_mul_le
+ sup_support_coeff_multisetProd_le
+ support_coeff_C_mul_T_of_ne_zero
+ support_coeff_divOf
+ support_coeff_mul_single
+ support_coeff_mul_single_eq_image
+ support_coeff_mul_single_subset
+ support_coeff_mul_subset
+ support_coeff_one
+ support_coeff_one_subset
+ support_coeff_single_mul
+ support_coeff_single_mul_eq_image
+ support_coeff_single_mul_subset
+ support_coeff_toLaurent
+ support_mapDomain_embedding
+ uniqueLinearEquiv
+ uniqueRingEquiv_symm_apply
++ instance : Module.Free R S[M] := .of_equiv (coeffLinearEquiv _).symm
++ mem_span_support_coeff
+++++-----+ symm_mk
++++-----+ symm_mk.aux
++-- moduleFinite
+-+- mem_adjoin_support
+-+- support_neg
- addCommMonoid
- apply_add_of_supDegree_le
- apply_eq_of_leftRegular_eq_of_generator
- apply_eq_zero_of_not_le_supDegree
- apply_supDegree_add_supDegree
- coeff
- coeff_rTensorAlgHom_monomial_tmul
- coeff_rTensorAlgHom_tmul
- domCongr_apply
- inhabited
- instCoeFun
- instance :
- instance [DecidableEq R] : DecidableEq R[X]
- instance _root_.AddMonoidAlgebra.instMul [Add M] : Mul (AddMonoidAlgebra R M)
- instance {σ : Type*} {R : Type*} [CommSemiring R]
- iterToSum_sumToIter
- le_inf_support_add
- le_inf_support_finset_prod
- le_inf_support_mul
- le_inf_support_multiset_prod
- mapAddEquiv_apply
- mapAlgHom_apply
- mapDomainAddEquiv_apply
- mapDomainRingEquiv_apply
- mapRangeRingHom_apply
- mapRange_eq_map
- mapRingEquiv_apply
- mapRingHom_apply
- mem_span_support'
- modOf_apply_add_self
- modOf_apply_of_exists_add
- modOf_apply_of_not_exists_add
- modOf_apply_self_add
- mul_apply_mul_eq_mul_of_uniqueMul
- mul_single_apply_aux
- nontrivial
- ofCoeff
- ofMulAction_apply
- ofMulAction_self_smul_eq_mul
- pderiv_sumToIter
- rTensor
- rTensorAlgEquiv_apply
- rTensorAlgHom
- rTensorAlgHom_apply_eq
- rTensorAlgHom_toLinearMap
- rTensor_apply
- rTensor_apply_X_tmul
- rTensor_apply_monomial_tmul
- rTensor_apply_tmul
- rTensor_apply_tmul_apply
- rTensor_symm_apply_single
- scalarRTensor
- scalarRTensor_apply_X_tmul_apply
- scalarRTensor_apply_monomial_tmul
- scalarRTensor_apply_tmul
- scalarRTensor_apply_tmul_apply
- scalarRTensor_symm_apply_single
- single_apply
- single_mul_apply_aux
- sumToIter_iterToSum
- sup_support_add_le
- sup_support_finset_prod_le
- sup_support_mul_le
- sup_support_multiset_prod_le
- support_C_mul_T_of_ne_zero
- support_mul
- support_mul_single
- support_mul_single_eq_image
- support_mul_single_subset
- support_one
- support_one_subset
- support_single_mul
- support_single_mul_eq_image
- support_single_mul_subset
- toLaurent_support
- unique
-- instance : Module.Free R S[M] := .finsupp ..
-- mem_span_support

You can run this locally as follows

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

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

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

Decrease in tech debt: (relative, absolute) = (0.61, 0.28)

Current number	Change	Type
445	-6	porting notes
165	-1	adaptation notes
647	6	erw
11	1	maxHeartBeats modifications
3	-1	backward.inferInstanceAs.wrap
6382	-12	backward.isDefEq.respectTransparency
46	-1	dsimp +instances

Current commit d8d00bddb5
Reference commit 044631201f

You can run this locally as

./scripts/reporting/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/MonoidAlgebra/Defs.lean

leanprover-community-bot-assistant · 2025-07-05T07:55:04Z

This pull request has conflicts, please merge master and resolve them.

leanprover-community-bot-assistant · 2025-07-05T10:46:17Z

This pull request has conflicts, please merge master and resolve them.

leanprover-community-bot-assistant · 2025-07-11T20:09:58Z

This pull request has conflicts, please merge master and resolve them.

eric-wieser · 2025-07-14T09:39:57Z

Is it a conscious choice not to do AddMonoidAlgebra at the same time?

leanprover-community-bot-assistant · 2025-07-23T00:34:57Z

This pull request has conflicts, please merge master and resolve them.

mathlib4-merge-conflict-bot · 2026-01-19T10:17:01Z

This pull request has conflicts, please merge master and resolve them.

mathlib4-merge-conflict-bot · 2026-01-20T10:01:22Z

This pull request has conflicts, please merge master and resolve them.

mathlib4-merge-conflict-bot · 2026-01-21T07:59:53Z

This pull request has conflicts, please merge master and resolve them.

mathlib4-merge-conflict-bot · 2026-01-26T17:05:49Z

This pull request has conflicts, please merge master and resolve them.

mathlib-merge-conflicts · 2026-02-03T22:00:18Z

This pull request has conflicts, please merge master and resolve them.

mathlib-merge-conflicts · 2026-02-15T13:26:13Z

This pull request has conflicts, please merge master and resolve them.

mathlib-merge-conflicts · 2026-02-17T23:36:04Z

This pull request has conflicts, please merge master and resolve them.

mathlib-merge-conflicts · 2026-03-02T18:24:53Z

This pull request has conflicts, please merge master and resolve them.

mathlib-merge-conflicts · 2026-03-05T12:02:51Z

This pull request has conflicts, please merge master and resolve them.

mathlib-merge-conflicts · 2026-03-10T07:34:34Z

This pull request has conflicts, please merge master and resolve them.

mathlib-merge-conflicts · 2026-03-13T00:02:35Z

This pull request has conflicts, please merge master and resolve them.

mathlib-dependent-issues · 2026-03-15T14:06:56Z

This PR/issue depends on:

~~[Merged by Bors] - chore(Algebra/Equiv/TransferInstance): split according to algebraic structures #26732~~
~~[Merged by Bors] - feat(Shrink): IsCancelMul instance #28407~~
~~[Merged by Bors] - feat(GroupWithZero/Action): transfer across equivs #28460~~
~~[Merged by Bors] - chore: tag Finsupp.prod_congr with gcongr #28511~~
~~[Merged by Bors] - chore(MonoidAlgebra/Defs): reorder, rename variables #29207~~
~~[Merged by Bors] - feat(Algebra/MonoidAlgebra): extend the R[M] notation to MonoidAlgebra R M #30877~~
~~[Merged by Bors] - chore: make Equiv.unique reducible #31143~~
~~[Merged by Bors] - feat: transfer FaithfulSMul/NoZeroSMulDivisors along equivs #31144~~
~~[Merged by Bors] - feat: Finsupp.sum in opposite monoid #32253~~
~~[Merged by Bors] - feat(Algebra/MonoidAlgebra): complete the map API #32254~~
~~[Merged by Bors] - chore(Algebra/MonoidAlgebra): use to_additive more #32398~~
~~[Merged by Bors] - chore: additivise MulOpposite.op_finsuppSum to itself #32501~~
~~[Merged by Bors] - feat(Algebra/MonoidAlgebra): single as a DistribMulActionHom #32508~~
~~[Merged by Bors] - chore(Data/Finsupp): rename the toFun projection to apply in simps #32562~~
~~[Merged by Bors] - feat(Algebra/MonoidAlgebra): cardinality of monoid algebras #32588~~
~~[Merged by Bors] - chore(Algebra/MonoidAlgebra): scope Algebra R[M] A[M] instance #32591~~
~~[Merged by Bors] - feat(Data/Finsupp): characterise default #32592~~
~~[Merged by Bors] - chore(Algebra/MonoidAlgebra): reduce dependence on defeq abuse, golf #32604~~
~~[Merged by Bors] - feat(RingTheory): transfer Coalgebra across an Equiv #32965~~
~~[Merged by Bors] - feat(Algebra): product of 1s over a Finsupp #33093~~
~~[Merged by Bors] - chore(Algebra/Group/TransferInstance): make mulEquiv_symm_apply be simp #33094~~
~~[Merged by Bors] - chore(RingTheory/FiniteType): move MonoidAlgebra lemmas earlier #33099~~
~~[Merged by Bors] - chore(Algebra/MonoidAlgebra): don't use hom classes when bundling mapDomain #33137~~
~~[Merged by Bors] - feat: transfer Coalgebra.IsCocomm across an Equiv #33139~~
~~[Merged by Bors] - chore(RingTheory/Coalgebra/MonoidAlgebra): use to_additive #33141~~
~~[Merged by Bors] - chore(RingTheory/Bialgebra/MonoidAlgebra): use to_additive #33452~~
~~[Merged by Bors] - feat(Algebra/Group/Equiv): MulEquiv.funUnique #33453~~
~~[Merged by Bors] - feat(RingTheory/TensorProduct/MonoidAlgebra): additivise #33482~~
~~[Merged by Bors] - feat(Algebra/MonoidAlgebra): R[M][N] ≃+* R[N][M] #33492~~
~~[Merged by Bors] - feat(Data/Finsupp): more API for sumElim #36675~~
refactor(Algebra/MonoidAlgebra): use coeff/ofCoeff more #36746
By Dependent Issues (🤖). Happy coding!

mathlib-merge-conflicts · 2026-03-15T14:35:40Z

This pull request has conflicts, please merge master and resolve them.

mathlib-merge-conflicts · 2026-03-20T06:40:13Z

This pull request has conflicts, please merge master and resolve them.

JovanGerb · 2026-03-20T15:57:33Z

Mathlib/Algebra/Polynomial/Degree/Defs.lean

+  simp only [erase_def, AddMonoidAlgebra.erase, AddMonoidAlgebra.coeff, AddMonoidAlgebra.ofCoeff,
+    degree, support]


Do I understand correctly that this proof will break when we switch to MonoidAlgebra being a structure? Is it possible to write a proof that works now and will continue to work?

Correct. Yes it might be possible, but I have already spent several hundred hours on this refactor so I don't want to sink any more time in proofs which I know how to write correctly post-refactor.

Did you mean to write this on one of the preliminary PRs btw? This PR is precisely the place where this proof will need changing

mathlib-merge-conflicts · 2026-03-21T19:03:57Z

This pull request has conflicts, please merge master and resolve them.

mathlib-merge-conflicts · 2026-03-24T04:24:40Z

This pull request has conflicts, please merge master and resolve them.

mathlib-merge-conflicts · 2026-03-26T17:58:36Z

This pull request has conflicts, please merge master and resolve them.

mathlib-merge-conflicts · 2026-04-05T05:42:43Z

This pull request has conflicts, please merge master and resolve them.

mathlib-merge-conflicts · 2026-04-07T12:06:43Z

This pull request has conflicts, please merge master and resolve them.

mathlib-merge-conflicts · 2026-04-13T20:54:37Z

This pull request has conflicts, please merge master and resolve them.

…useful In essence, this changes the RHS from having support `univ` to having support `{1}`. These are equal, but having the RHS be `single 1 r` is much more useful in practice.

…/from `Finsupp` Introduce `coeff : R[M] → M →₀ R` and `ofCoeff : (M →₀ R) → R[M]` as a way to convert explicitly between `MonoidAlgebra` and `Finsupp` and thus avoiding defeq abuse. This is a fast and loose preliminary version of #25273. In particular, some proofs break and need to be fixed with either `set_option backward.isDefEq.respectTransparency false`, or by unfolding `MvPolynomial`. The situation will improve again once #25273 is in and further `MvPolynomial` is turned into an `abbrev`. All the changes beyond introducing `coeff`/`ofCoeff` and using them in the basic API are motivated by fixing downstream breakage.

github-actions bot added large-import Automatically added label for PRs with a significant increase in transitive imports t-algebra Algebra (groups, rings, fields, etc) labels May 28, 2025

eric-wieser reviewed May 29, 2025

View reviewed changes

Mathlib/Algebra/MonoidAlgebra/Defs.lean Outdated Show resolved Hide resolved

mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jul 4, 2025

YaelDillies force-pushed the linear_combination_of branch from 1228933 to b39d040 Compare July 4, 2025 16:56

YaelDillies changed the title ~~feat: Finsupp.linearCombination MonoidAlgebra.of = id~~ refactor: make MonoidAlgebra into a one-field structure Jul 4, 2025

YaelDillies added the WIP Work in progress label Jul 4, 2025

github-actions bot added the file-removed A Lean module was (re)moved without a `deprecated_module` annotation label Jul 4, 2025

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 5, 2025

YaelDillies force-pushed the linear_combination_of branch from b39d040 to 3578d1d Compare July 5, 2025 08:47

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 5, 2025

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 5, 2025

YaelDillies force-pushed the linear_combination_of branch from 3578d1d to 653ea1d Compare July 5, 2025 10:59

github-actions bot removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) file-removed A Lean module was (re)moved without a `deprecated_module` annotation labels Jul 5, 2025

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 11, 2025

YaelDillies force-pushed the linear_combination_of branch from 653ea1d to 0debcb5 Compare July 12, 2025 06:12

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 12, 2025

mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jul 14, 2025

YaelDillies force-pushed the linear_combination_of branch from 0debcb5 to 75c9ab5 Compare July 14, 2025 06:33

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 23, 2025

YaelDillies force-pushed the linear_combination_of branch from 75c9ab5 to 9cccd73 Compare July 23, 2025 07:09

leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 23, 2025

mathlib4-merge-conflict-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Aug 13, 2025

YaelDillies mentioned this pull request Mar 16, 2026

refactor(Algebra/MonoidAlgebra): use coeff/ofCoeff more #36746

Open

7 tasks

YaelDillies mentioned this pull request Mar 20, 2026

[Merged by Bors] - feat(Algebra/MonoidAlgebra): erase and update #36848

Closed

JovanGerb reviewed Mar 20, 2026

View reviewed changes

YaelDillies mentioned this pull request Apr 7, 2026

[Merged by Bors] - feat(Algebra/MonoidAlgebra): a few lemmas #37750

Closed

YaelDillies added 6 commits April 14, 2026 09:57

chore: syntactically generalise symm_mk

8944b1a

chore(Algebra/MonoidAlgebra): make uniqueRingEquiv_symm_apply more …

8adfb3e

…useful In essence, this changes the RHS from having support `univ` to having support `{1}`. These are equal, but having the RHS be `single 1 r` is much more useful in practice.

broken

15e1b36

refactor: make MonoidAlgebra into a one-field structure

ed193c6

broken

d8d00bd

		simp only [erase_def, AddMonoidAlgebra.erase, AddMonoidAlgebra.coeff, AddMonoidAlgebra.ofCoeff,
		degree, support]

Conversation

YaelDillies commented May 28, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

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

Uh oh!

PR summary 044631201f

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

leanprover-community-bot-assistant commented Jul 5, 2025

Uh oh!

leanprover-community-bot-assistant commented Jul 5, 2025

Uh oh!

leanprover-community-bot-assistant commented Jul 11, 2025

Uh oh!

eric-wieser commented Jul 14, 2025

Uh oh!

leanprover-community-bot-assistant commented Jul 23, 2025

Uh oh!

mathlib4-merge-conflict-bot commented Jan 19, 2026

Uh oh!

mathlib4-merge-conflict-bot commented Jan 20, 2026

Uh oh!

mathlib4-merge-conflict-bot commented Jan 21, 2026

Uh oh!

mathlib4-merge-conflict-bot commented Jan 26, 2026

Uh oh!

mathlib-merge-conflicts bot commented Feb 3, 2026

Uh oh!

mathlib-merge-conflicts bot commented Feb 15, 2026

Uh oh!

mathlib-merge-conflicts bot commented Feb 17, 2026

Uh oh!

mathlib-merge-conflicts bot commented Mar 2, 2026

Uh oh!

mathlib-merge-conflicts bot commented Mar 5, 2026

Uh oh!

mathlib-merge-conflicts bot commented Mar 10, 2026

Uh oh!

mathlib-merge-conflicts bot commented Mar 13, 2026

Uh oh!

mathlib-dependent-issues bot commented Mar 15, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

mathlib-merge-conflicts bot commented Mar 15, 2026

Uh oh!

mathlib-merge-conflicts bot commented Mar 20, 2026

Uh oh!

JovanGerb Mar 20, 2026

Choose a reason for hiding this comment

Uh oh!

YaelDillies Mar 20, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

mathlib-merge-conflicts bot commented Mar 21, 2026

Uh oh!

mathlib-merge-conflicts bot commented Mar 24, 2026

Uh oh!

mathlib-merge-conflicts bot commented Mar 26, 2026

Uh oh!

mathlib-merge-conflicts bot commented Apr 5, 2026

Uh oh!

mathlib-merge-conflicts bot commented Apr 7, 2026

Uh oh!

mathlib-merge-conflicts bot commented Apr 13, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

8 participants

YaelDillies commented May 28, 2025 •

edited

Loading

github-actions bot commented May 28, 2025 •

edited

Loading

mathlib-dependent-issues bot commented Mar 15, 2026 •

edited

Loading

YaelDillies Mar 20, 2026 •

edited

Loading