refactor(Algebra/Polynomial): make into an `abbrev` of `AddMonoidAlgebra` by YaelDillies · Pull Request #41981 · leanprover-community/mathlib4

YaelDillies · 2026-07-21T14:16:02Z

... and deprecate the declarations that are now tautological (toFinsupp/ofFinsupp, coeff and their API). For some of the Polynomial declarations that needed changing, it was simplest to replace them with the corresponding AddMonoidAlgebra one. Note that this replacement is far from exhaustive (a majority of the Polynomial API could be replaced this way).

Note that algebraMap R R[X] has changed defeq.

Zulip

Generated through several rounds of manual review with Claude Opus. Heavily edited by hand afterwards.

Assisted-by: Claude Opus 4.8

github-actions · 2026-07-21T14:17:41Z

PR summary 652861bf80

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.LinearAlgebra.Finsupp.VectorSpace	1229	1217	-12 (-0.98%)

Import changes for all files

Files	Import difference
11 files `Mathlib.Algebra.Category.ModuleCat.Projective` `Mathlib.Algebra.Category.ModuleCat.Ulift` `Mathlib.Algebra.Module.Presentation.Free` `Mathlib.Algebra.Module.Projective` `Mathlib.LinearAlgebra.DirectSum.Basis` `Mathlib.LinearAlgebra.Finsupp.VectorSpace` `Mathlib.LinearAlgebra.LinearIndependent.BaseChange` `Mathlib.LinearAlgebra.Matrix.StdBasis` `Mathlib.LinearAlgebra.StdBasis` `Mathlib.LinearAlgebra.TensorProduct.Basis` `Mathlib.Topology.Algebra.SeparationQuotient.Section`	-12
3 files `Mathlib.Algebra.Category.ModuleCat.Ext.DimensionShifting` `Mathlib.Algebra.Category.ModuleCat.Ext.HasExt` `Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension`	-11
`Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion` `Mathlib.LinearAlgebra.PiTensorProduct.Basis`	-10
110 files `Mathlib.Algebra.AffineMonoid.Embedding` `Mathlib.Algebra.Algebra.Subalgebra.Centralizer` `Mathlib.Algebra.Azumaya.Defs` `Mathlib.Algebra.Azumaya.Matrix` `Mathlib.Algebra.Category.ModuleCat.Ext.Baer` `Mathlib.Algebra.Category.ModuleCat.Ext.Basic` `Mathlib.Algebra.Category.ModuleCat.Ext.Finite` `Mathlib.Algebra.Category.ModuleCat.Free` `Mathlib.Algebra.Category.ModuleCat.Topology.Basic` `Mathlib.Algebra.Category.ModuleCat.Topology.Homology` `Mathlib.Algebra.Category.Ring.FilteredColimitsLocal` `Mathlib.Algebra.DualQuaternion` `Mathlib.Algebra.Homology.LocalCohomology` `Mathlib.Algebra.Jordan.Basic` `Mathlib.Algebra.Lie.Abelian` `Mathlib.Algebra.Lie.AdjointAction.Derivation` `Mathlib.Algebra.Lie.BaseChange` `Mathlib.Algebra.Lie.Cochain` `Mathlib.Algebra.Lie.Derivation.Basic` `Mathlib.Algebra.Lie.DirectSum` `Mathlib.Algebra.Lie.Extension` `Mathlib.Algebra.Lie.Graded` `Mathlib.Algebra.Lie.IdealOperations` `Mathlib.Algebra.Lie.Ideal` `Mathlib.Algebra.Lie.Normalizer` `Mathlib.Algebra.Lie.OfAssociative` `Mathlib.Algebra.Lie.Prod` `Mathlib.Algebra.Lie.Quotient` `Mathlib.Algebra.Lie.SemiDirect` `Mathlib.Algebra.Lie.Subalgebra` `Mathlib.Algebra.Lie.Submodule` `Mathlib.Algebra.Lie.TensorProduct` `Mathlib.Algebra.Module.LinearMap.FiniteRange` `Mathlib.Algebra.Module.SpanRank` `Mathlib.Algebra.QuadraticAlgebra.BaseChange` `Mathlib.Algebra.QuadraticAlgebra.Basic` `Mathlib.Algebra.QuadraticAlgebra.Defs` `Mathlib.Algebra.QuaternionBasis` `Mathlib.Algebra.Quaternion` `Mathlib.Algebra.Symmetrized` `Mathlib.Data.ZMod.QuotientRing` `Mathlib.FieldTheory.Finiteness` `Mathlib.FieldTheory.Tower` `Mathlib.GroupTheory.FreeGroup.GeneratorEquiv` `Mathlib.LinearAlgebra.Basis.MulOpposite` `Mathlib.LinearAlgebra.Dimension.Constructions` `Mathlib.LinearAlgebra.Dimension.Finite` `Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition` `Mathlib.LinearAlgebra.Dimension.Free` `Mathlib.LinearAlgebra.Dimension.LinearMap` `Mathlib.LinearAlgebra.Dimension.OrzechProperty` `Mathlib.LinearAlgebra.Dimension.RankNullity` `Mathlib.LinearAlgebra.Dimension.StrongRankCondition` `Mathlib.LinearAlgebra.FiniteDimensional.Basic` `Mathlib.LinearAlgebra.FiniteDimensional.Defs` `Mathlib.LinearAlgebra.FreeModule.Finite.Basic` `Mathlib.LinearAlgebra.FreeModule.Int` `Mathlib.LinearAlgebra.FreeModule.PID` `Mathlib.LinearAlgebra.InvariantBasisNumber` `Mathlib.LinearAlgebra.Matrix.Dual` `Mathlib.LinearAlgebra.Matrix.ToLin` `Mathlib.LinearAlgebra.Projectivization.Basic` `Mathlib.LinearAlgebra.Projectivization.Cardinality` `Mathlib.LinearAlgebra.Projectivization.Collinear` `Mathlib.LinearAlgebra.Projectivization.Independence` `Mathlib.LinearAlgebra.Projectivization.Subspace` `Mathlib.NumberTheory.FrobeniusNumber` `Mathlib.RingTheory.Adjoin.Dimension` `Mathlib.RingTheory.Artinian.Module` `Mathlib.RingTheory.Artinian.Ring` `Mathlib.RingTheory.Coalgebra.IsFrobenius` `Mathlib.RingTheory.FiniteLength` `Mathlib.RingTheory.Finiteness.Cardinality` `Mathlib.RingTheory.Finiteness.Cofinite` `Mathlib.RingTheory.Finiteness.NilpotentKer` `Mathlib.RingTheory.Finiteness.Nilpotent` `Mathlib.RingTheory.Finiteness.Projective` `Mathlib.RingTheory.GradedAlgebra.Noetherian` `Mathlib.RingTheory.Ideal.AssociatedPrime.Basic` `Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness` `Mathlib.RingTheory.Ideal.MinimalPrime.Colon` `Mathlib.RingTheory.Ideal.MinimalPrime.Localization` `Mathlib.RingTheory.Ideal.NatInt` `Mathlib.RingTheory.Ideal.Quotient.Index` `Mathlib.RingTheory.Ideal.Quotient.Nilpotent` `Mathlib.RingTheory.Ideal.Quotient.Noetherian` `Mathlib.RingTheory.KrullDimension.Basic` `Mathlib.RingTheory.KrullDimension.Field` `Mathlib.RingTheory.Lasker` `Mathlib.RingTheory.Length` `Mathlib.RingTheory.LocalProperties.Submodule` `Mathlib.RingTheory.LocalRing.LocalSubring` `Mathlib.RingTheory.LocalRing.MaximalIdeal.Square` `Mathlib.RingTheory.LocalRing.ResidueField.Basic` `Mathlib.RingTheory.Localization.AsSubring` `Mathlib.RingTheory.Localization.AtPrime.Basic` `Mathlib.RingTheory.Localization.LocalizationLocalization` `Mathlib.RingTheory.Nilpotent.Lemmas` `Mathlib.RingTheory.Noetherian.Basic` `Mathlib.RingTheory.Noetherian.Nilpotent` `Mathlib.RingTheory.Noetherian.Orzech` `Mathlib.RingTheory.OrzechProperty` `Mathlib.RingTheory.SimpleModule.InjectiveProjective` `Mathlib.RingTheory.SimpleModule.WedderburnArtin` `Mathlib.RingTheory.Spectrum.Prime.Basic` `Mathlib.RingTheory.SurjectiveOnStalks` `Mathlib.RingTheory.TensorProduct.Free` `Mathlib.RingTheory.ZMod` `Mathlib.Topology.Algebra.Module.ModuleTopology` `Mathlib.Topology.Algebra.Projectivization`	-8
12 files `Mathlib.Algebra.AffineMonoid.UniqueSums` `Mathlib.Analysis.Normed.Operator.Compact.Basic` `Mathlib.Analysis.Normed.Operator.Compact` `Mathlib.LinearAlgebra.Complex.FiniteDimensional` `Mathlib.LinearAlgebra.Complex.Module` `Mathlib.NumberTheory.Padics.Measure.Topology` `Mathlib.Topology.Algebra.ContinuousAffineMap.Topology` `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`	-7
27 files `Mathlib.Analysis.CStarAlgebra.Classes` `Mathlib.Analysis.Complex.AbelLimit` `Mathlib.Analysis.Complex.Asymptotics` `Mathlib.Analysis.Complex.Basic` `Mathlib.Analysis.Complex.HalfPlane` `Mathlib.Analysis.Complex.IntegerCompl` `Mathlib.Analysis.Complex.ReImTopology` `Mathlib.Analysis.Complex.Spectrum` `Mathlib.Analysis.Complex.UpperHalfPlane.Basic` `Mathlib.Analysis.SpecialFunctions.Artanh` `Mathlib.Analysis.SpecialFunctions.Exp` `Mathlib.Analysis.SpecialFunctions.Log.Basic` `Mathlib.CategoryTheory.Preadditive.HomOrthogonal` `Mathlib.LinearAlgebra.Dimension.ErdosKaplansky` `Mathlib.LinearAlgebra.Dimension.Torsion.Basic` `Mathlib.LinearAlgebra.Dimension.Torsion.Finite` `Mathlib.LinearAlgebra.Matrix.Basis` `Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber` `Mathlib.LinearAlgebra.Matrix.Nonsingular` `Mathlib.LinearAlgebra.PiTensorProduct.Dual` `Mathlib.LinearAlgebra.Projectivization.Constructions` `Mathlib.LinearAlgebra.TensorProduct.Matrix` `Mathlib.MeasureTheory.Constructions.BorelSpace.Complex` `Mathlib.MeasureTheory.Measure.Complex` `Mathlib.ModelTheory.Arithmetic.Presburger.Definability` `Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic` `Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt`	-6
140 files `Mathlib.Analysis.Analytic.Basic` `Mathlib.Analysis.Analytic.CPolynomialDef` `Mathlib.Analysis.Analytic.CPolynomial` `Mathlib.Analysis.Analytic.ChangeOrigin` `Mathlib.Analysis.Analytic.Composition` `Mathlib.Analysis.Analytic.Constructions` `Mathlib.Analysis.Analytic.ConvergenceRadius` `Mathlib.Analysis.Analytic.Inverse` `Mathlib.Analysis.Analytic.IsolatedZeros` `Mathlib.Analysis.Analytic.IteratedFDeriv` `Mathlib.Analysis.Analytic.Linear` `Mathlib.Analysis.Analytic.OfScalars` `Mathlib.Analysis.Analytic.Order` `Mathlib.Analysis.Analytic.Uniqueness` `Mathlib.Analysis.Analytic.Within` `Mathlib.Analysis.BoxIntegral.Partition.Additive` `Mathlib.Analysis.Calculus.AbsolutelyMonotone` `Mathlib.Analysis.Calculus.AddTorsor.AffineMap` `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.RestrictScalars` `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.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.DiffContOnCl` `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.Linear` `Mathlib.Analysis.Calculus.FDeriv.Mul` `Mathlib.Analysis.Calculus.FDeriv.OfCompLeft` `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.FormalMultilinearSeries` `Mathlib.Analysis.Calculus.InverseFunctionTheorem.Analytic` `Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn` `Mathlib.Analysis.Calculus.InverseFunctionTheorem.Deriv` `Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv` `Mathlib.Analysis.Calculus.IteratedDeriv.Analytic` `Mathlib.Analysis.Calculus.IteratedDeriv.Defs` `Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno` `Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas` `Mathlib.Analysis.Calculus.IteratedDeriv.WithinZpow` `Mathlib.Analysis.Calculus.LagrangeMultipliers` `Mathlib.Analysis.Calculus.LineDeriv.Basic` `Mathlib.Analysis.Calculus.LocalExtr.Basic` `Mathlib.Analysis.Calculus.LocalExtr.LineDeriv` `Mathlib.Analysis.Calculus.LocalExtr.Rolle` `Mathlib.Analysis.LocallyConvex.PointwiseConvergence` `Mathlib.Analysis.LocallyConvex.StrongTopology` `Mathlib.Analysis.Normed.Affine.ContinuousAffineMap` `Mathlib.Analysis.Normed.Algebra.Logarithm` `Mathlib.Analysis.Normed.Algebra.Unitization` `Mathlib.Analysis.Normed.Group.ZeroAtInfty` `Mathlib.Analysis.Normed.Module.Alternating.Basic` `Mathlib.Analysis.Normed.Module.Alternating.Curry` `Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin` `Mathlib.Analysis.Normed.Module.Complemented` `Mathlib.Analysis.Normed.Module.Completion` `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.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.Completeness` `Mathlib.Analysis.Normed.Operator.Extend` `Mathlib.Analysis.Normed.Operator.Mul` `Mathlib.Analysis.Normed.Operator.NNNorm` `Mathlib.Analysis.Normed.Operator.NormedSpace` `Mathlib.Analysis.Normed.Operator.Prod` `Mathlib.Analysis.ODE.Basic` `Mathlib.Analysis.ODE.Transform` `Mathlib.Analysis.SpecialFunctions.Sqrt` `Mathlib.Geometry.Manifold.ConformalGroupoid` `Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic` `Mathlib.RingTheory.MvPolynomial.Basic` `Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous` `Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion` `Mathlib.Topology.Algebra.Module.Alternating.Topology` `Mathlib.Topology.Algebra.Module.Multilinear.Topology` `Mathlib.Topology.Category.Profinite.Nobeling.Induction` `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.StarOrdered` `Mathlib.Topology.ContinuousMap.ZeroAtInftyUnitization` `Mathlib.Topology.ContinuousMap.ZeroAtInfty` `Mathlib.Topology.MetricSpace.GromovHausdorffRealized` `Mathlib.Topology.MetricSpace.Ultra.ContinuousMaps` `Mathlib.Topology.MetricSpace.UniformConvergence` `Mathlib.Topology.TietzeExtension` `Mathlib.Topology.VectorBundle.Basic` `Mathlib.Topology.VectorBundle.Constructions` `Mathlib.Topology.VectorBundle.ContinuousAlternatingMap` `Mathlib.Topology.VectorBundle.FiniteDimensional` `Mathlib.Topology.VectorBundle.Hom`	-5
65 files `Mathlib.Analysis.CStarAlgebra.ContinuousMap` `Mathlib.Analysis.CStarAlgebra.Exponential` `Mathlib.Analysis.CStarAlgebra.Unitization` `Mathlib.Analysis.Calculus.Conformal.InnerProduct` `Mathlib.Analysis.Calculus.ContDiff.RCLike` `Mathlib.Analysis.Calculus.Deriv.MeanValue` `Mathlib.Analysis.Calculus.DerivativeTest` `Mathlib.Analysis.Calculus.DifferentialForm.Basic` `Mathlib.Analysis.Calculus.DifferentialForm.VectorField` `Mathlib.Analysis.Calculus.FDeriv.Extend` `Mathlib.Analysis.Calculus.FDeriv.Partial` `Mathlib.Analysis.Calculus.FDeriv.Symmetric` `Mathlib.Analysis.Calculus.InverseFunctionTheorem.ContDiff` `Mathlib.Analysis.Calculus.LHopital` `Mathlib.Analysis.Calculus.LogDeriv` `Mathlib.Analysis.Calculus.MeanValue` `Mathlib.Analysis.Calculus.SmoothSeries` `Mathlib.Analysis.Calculus.UniformLimitsDeriv` `Mathlib.Analysis.Calculus.VectorField` `Mathlib.Analysis.Complex.Convex` `Mathlib.Analysis.Complex.RealDeriv` `Mathlib.Analysis.Convex.Deriv` `Mathlib.Analysis.Convex.Strong` `Mathlib.Analysis.InnerProductSpace.Affine` `Mathlib.Analysis.InnerProductSpace.Basic` `Mathlib.Analysis.InnerProductSpace.Completion` `Mathlib.Analysis.InnerProductSpace.ConformalLinearMap` `Mathlib.Analysis.InnerProductSpace.Continuous` `Mathlib.Analysis.InnerProductSpace.Convex` `Mathlib.Analysis.InnerProductSpace.LinearMap` `Mathlib.Analysis.InnerProductSpace.OfNorm` `Mathlib.Analysis.InnerProductSpace.Projection.Minimal` `Mathlib.Analysis.Meromorphic.Basic` `Mathlib.Analysis.Meromorphic.Divisor` `Mathlib.Analysis.Meromorphic.FactorizedRational` `Mathlib.Analysis.Meromorphic.IsolatedZeros` `Mathlib.Analysis.Meromorphic.LogDeriv` `Mathlib.Analysis.Meromorphic.NormalForm` `Mathlib.Analysis.Meromorphic.Order` `Mathlib.Analysis.Meromorphic.RCLike` `Mathlib.Analysis.Meromorphic.TrailingCoefficient` `Mathlib.Analysis.Normed.Algebra.Exponential` `Mathlib.Analysis.Normed.Module.RCLike.Basic` `Mathlib.Analysis.Normed.Module.RCLike.Extend` `Mathlib.Analysis.Normed.Module.RieszLemma` `Mathlib.Analysis.ODE.Gronwall` `Mathlib.Analysis.RCLike.BoundedContinuous` `Mathlib.Analysis.RCLike.ContinuousMap` `Mathlib.Analysis.SpecialFunctions.ExpDeriv` `Mathlib.Analysis.SpecialFunctions.Exponential` `Mathlib.Analysis.SpecialFunctions.Log.Deriv` `Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq` `Mathlib.Analysis.SpecialFunctions.Sigmoid` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Series` `Mathlib.Combinatorics.Derangements.Exponential` `Mathlib.Geometry.Euclidean.Inversion.Basic` `Mathlib.Geometry.Manifold.IsManifold.Basic` `Mathlib.Geometry.Manifold.LocalSourceTargetProperty` `Mathlib.MeasureTheory.Function.SpecialFunctions.Inner` `Mathlib.MeasureTheory.Function.StronglyMeasurable.Inner` `Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn` `Mathlib.Topology.ContinuousMap.ContinuousSqrt` `Mathlib.Topology.ContinuousMap.Ideals` `Mathlib.Topology.VectorBundle.Riemannian`	-4
3 files `Mathlib.Algebra.BrauerGroup.Defs` `Mathlib.Algebra.Lie.Free` `Mathlib.Algebra.Lie.UniversalEnveloping`	-3

Declarations diff (regex)

+ X_eq_single
+ card_support_coeff_mul_le
+ coeff_monomial_apply
+ eval₂_eq_liftNC
+ ofFinsupp
+ single_eq_monomial
+ support_ofCoeff
+ toFinsupp
+ toFinsuppIsoAlg_symm_apply_toFinsupp
+ toFinsuppIsoLinear_symm_apply_toFinsupp
- algebraOfAlgebra
- coeff
- commRing
- commSemiring
- distribMulAction
- distribSMul
- erase
- faithfulSMul
- inhabited
- instIntCast
- instNSMul
- instNatCast
- instZSMul
- instance (priority := 1) pow : Pow R[X] ℕ where pow p n := npowRec n p
- instance : Add R[X]
- instance : IsLocalHom (algebraMap R (Polynomial R))
- instance : Module.Free R R[X] := .of_equiv (Polynomial.toFinsuppIsoLinear _).symm
- instance : Mul R[X]
- instance : One R[X]
- instance : Zero R[X]
- instance [DecidableEq R] : DecidableEq R[X] := (toFinsuppIso R).toEquiv.decidableEq
- instance [IsCancelAdd R] [IsCancelMulZero R] : IsCancelMulZero R[X]
- instance [IsCancelAdd R] [IsDomain R] : IsDomain R[X]
- instance [IsCancelAdd R] [IsLeftCancelMulZero R] : IsLeftCancelMulZero R[X]
- instance [IsCancelAdd R] [IsRightCancelMulZero R] : IsRightCancelMulZero R[X]
- instance [NoZeroDivisors R] : NoZeroDivisors R[X]
- instance {R : Type u} [Ring R] : Neg R[X]
- instance {R : Type u} [Ring R] : Sub R[X]
- instance {S : Type*} [Semiring S] [Module S R] [IsTorsionFree S R] : IsTorsionFree S R[X]
- isCentralScalar
- isScalarTower
- isScalarTower_right
- module
- nontrivial
- ring
- semiring
- smulCommClass
- smulZeroClass
- unique
- update

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

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

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

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean -- stale, waiting for the new build)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 4ee2a23).

+10 new declarations
−52 removed declarations

+AddMonoidAlgebra.card_support_coeff_mul_le
-AddMonoidAlgebra.comapDomainAddMonoidHom.congr_simp
+AddMonoidAlgebra.comapDomain_single_of_notMem_range
+MonoidAlgebra.card_support_coeff_mul_le
+Polynomial.X_eq_single
-Polynomial.algebraOfAlgebra
-Polynomial.casesOn
-Polynomial.coeff
+Polynomial.coeff_monomial_apply
-Polynomial.commRing
-Polynomial.commSemiring
-Polynomial.ctorIdx
-Polynomial.distribMulAction
-Polynomial.distribSMul
-Polynomial.erase
-Polynomial.erase_def
+Polynomial.eval₂_eq_liftNC
-Polynomial.faithfulSMul
-Polynomial.inhabited
-Polynomial.instAdd
-Polynomial.instDecidableEq
-Polynomial.instFree
-Polynomial.instIntCast
-Polynomial.instIsCancelMulZeroOfIsCancelAdd
-Polynomial.instIsDomainOfIsCancelAdd
-Polynomial.instIsLeftCancelMulZeroOfIsCancelAdd
-Polynomial.instIsLocalHomRingHomAlgebraMap
-Polynomial.instIsRightCancelMulZeroOfIsCancelAdd
-Polynomial.instIsTorsionFree
-Polynomial.instMul
-Polynomial.instNSMul
-Polynomial.instNatCast
-Polynomial.instNeg
-Polynomial.instNoZeroDivisors
-Polynomial.instOne
-Polynomial.instSub
-Polynomial.instZSMul
-Polynomial.instZero
-Polynomial.isCentralScalar
-Polynomial.isScalarTower
-Polynomial.isScalarTower_right
-Polynomial.module
-Polynomial.noConfusion
-Polynomial.noConfusionType
-Polynomial.nontrivial
-Polynomial.ofFinsupp.inj
-Polynomial.ofFinsupp.injEq
-Polynomial.ofFinsupp.noConfusion
-Polynomial.ofFinsupp.sizeOf_spec
-Polynomial.pow
-Polynomial.rec
-Polynomial.recOn
-Polynomial.ring
-Polynomial.semiring
+Polynomial.single_eq_monomial
-Polynomial.smulCommClass
-Polynomial.smulZeroClass
+Polynomial.support_ofCoeff
+Polynomial.toFinsuppIsoAlg_symm_apply
+Polynomial.toFinsuppIsoLinear_symm_apply
-Polynomial.unique
-Polynomial.update

Decrease in strong tech debt: (relative, absolute) = (4.00, 0.80)

Current number	Change	Type (strong)
5	-4	disabled deprecation lints

No changes to weak technical debt.

Current commit 652861bf80
Reference commit 6100109f1d

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.py 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).

tb65536 · 2026-07-23T16:44:32Z

!radar

leanprover-radar · 2026-07-23T16:44:50Z

Benchmark results for 4a299ac against 6e593ca are in. There are significant results. @tb65536

🟥 build//instructions: +127.2G (+0.09%)

Medium changes (11🟥)

🟥 build/module/Mathlib.Algebra.Polynomial.Bivariate//instructions: +3.8G (+13.50%)
🟥 build/module/Mathlib.Algebra.Polynomial.Derivative//instructions: +4.2G (+8.30%)
🟥 build/module/Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point//instructions: +10.8G (+15.89%)
🟥 build/module/Mathlib.FieldTheory.RatFunc.Basic//instructions: +8.3G (+5.94%)
🟥 build/module/Mathlib.LinearAlgebra.Semisimple//instructions: +8.4G (+20.35%)
🟥 build/module/Mathlib.NumberTheory.FLT.MasonStothers//instructions: +2.3G (+30.77%)
🟥 build/module/Mathlib.NumberTheory.RatFunc.Ostrowski//instructions: +4.8G (+11.76%)
🟥 build/module/Mathlib.RingTheory.Etale.StandardEtale//instructions: +10.2G (+18.59%)
🟥 build/module/Mathlib.RingTheory.LaurentSeries//instructions: +7.3G (+7.22%)
🟥 build/module/Mathlib.RingTheory.LocalRing.ResidueField.Polynomial//instructions: +6.5G (+17.31%)
🟥 build/module/Mathlib.RingTheory.Polynomial.Quotient//instructions: +2.8G (+11.57%)

Small changes (5✅, 26🟥)

🟥 build/module/Mathlib.Algebra.MvPolynomial.Equiv//instructions: +1.3G (+2.68%)
🟥 build/module/Mathlib.Algebra.Polynomial.AlgebraMap//instructions: +1.3G (+3.48%)
✅ build/module/Mathlib.Algebra.Polynomial.Basic//instructions: -6.0G (-16.16%) (reduced significance based on *//lines)
🟥 build/module/Mathlib.Algebra.Polynomial.Div//instructions: +1.5G (+4.24%)
🟥 build/module/Mathlib.Algebra.Polynomial.FieldDivision//instructions: +2.2G (+5.82%)
✅ build/module/Mathlib.Algebra.Polynomial.Monomial//instructions: -681.6M (-12.53%)
🟥 build/module/Mathlib.Algebra.Polynomial.PartialFractions//instructions: +862.3M (+3.56%)
🟥 build/module/Mathlib.Algebra.Polynomial.RuleOfSigns//instructions: +3.0G (+6.23%)
🟥 build/module/Mathlib.Algebra.Polynomial.Splits//instructions: +2.3G (+5.76%)
🟥 build/module/Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic//instructions: +1.5G (+7.26%)
🟥 build/module/Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula//instructions: +2.2G (+4.80%)
🟥 build/module/Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic//instructions: +3.7G (+12.02%)
🟥 build/module/Mathlib.FieldTheory.KummerExtension//instructions: +1.3G (+3.13%)
🟥 build/module/Mathlib.FieldTheory.RatFunc.AsPolynomial//instructions: +3.6G (+14.83%)
🟥 build/module/Mathlib.FieldTheory.RatFunc.Defs//instructions: +1.2G (+12.31%)
🟥 build/module/Mathlib.FieldTheory.RatFunc.Luroth//instructions: +3.1G (+6.18%)
✅ build/module/Mathlib.FieldTheory.SeparableClosure//instructions: -1.7G (-2.47%)
🟥 build/module/Mathlib.NumberTheory.FLT.Polynomial//instructions: +1.5G (+9.07%)
🟥 build/module/Mathlib.NumberTheory.KummerDedekind//instructions: +2.1G (+8.01%)
🟥 build/module/Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind//instructions: +1.7G (+7.74%)
and 11 more

tb65536 · 2026-07-23T17:12:23Z

@YaelDillies Is this what we were expecting? A minor slowdown as the price for resolving defeq issues?

YaelDillies · 2026-07-24T06:43:23Z

Almost. A minor slowdown as the price for unifying API. The unification cannot for the most part happen in this PR (not that we would want to as it would bloat the diff), because the type signatures in the API for Polynomial and AddMonoidAlgebra are currently subtly different, see #41544 for the current PR on that front.

mathlib-merge-conflicts · 2026-08-17T21:18:23Z

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

mathlib-merge-conflicts · 2026-09-02T19:37:03Z

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

mathlib-merge-conflicts · 2026-09-09T18:45:36Z

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

mathlib-merge-conflicts · 2026-09-15T20:25:04Z

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

mathlib-merge-conflicts · 2026-09-26T12:31:59Z

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

mathlib-merge-conflicts · 2026-09-28T04:52:58Z

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

mathlib-merge-conflicts · 2026-10-07T04:01:46Z

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

…bra` ... and deprecate the declarations that are now tautological (`toFinsupp`/`ofFinsupp` and their API). For some of the `Polynomial` declarations that needed changing, it was simplest to replace them with the corresponding `AddMonoidAlgebra` one. Note that this replacement is far from exhaustive (a majority of the `Polynomial` API could be replaced this way). Note that `algebraMap R R[X]` has changed defeq. Generated through several rounds of manual review with Claude Opus. Heavily edited by hand afterwards. [Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Reworking.20Finsupp.2C.20MonoidAlgebra.2C.20HahnSeries.2E.20PowerSeries/with/609275708) Assisted-by: Claude Opus 4.8

mathlib-merge-conflicts · 2026-10-16T11:58:24Z

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

jjdishere · 2026-10-24T17:08:22Z

I was checking Lean diff for declarations missing deprecations. The following declarations should have a deprecation:

Polynomial.coeff
Polynomial.coeff_inj
Polynomial.coeff_injective
Polynomial.coeff_one_zero
Polynomial.erase
Polynomial.erase_def
Polynomial.erase_zero
Polynomial.eval₂_ofFinsupp
Polynomial.finite_range_coeff
Polynomial.toFinsuppIsoAlg_symm_apply_toFinsupp
Polynomial.toFinsuppIsoLinear_symm_apply_toFinsupp
Polynomial.update

jjdishere · 2026-10-24T17:35:53Z

Polynomial.coeff_one_zero was unintentionally removed, right? It should remain like Polynomial.coeff_zero.

As a result, many AddMonoidAlgebra.coeff_one_zero appears in the diff should change back to coeff_one_zero.

I don't mean that we should copy APIs into Polynomial namespace. I suggest that we should split these changes (removing APIs in Polynomial) into another PR.

jjdishere

I've gone through all the diff. Thanks!

jjdishere · 2026-10-24T17:38:58Z

 theorem iterate_derivative_prod_X_sub_C {k : ℕ} {S : Finset R} (hk : k ≤ #S) :
    derivative^[k] (∏ a ∈ S, (X - C a)) =
-    k.factorial * ∑ T ∈ S.powersetCard (#S - k), ∏ a ∈ T, (X - C a) := by
+    ↑(k.factorial) * ∑ T ∈ S.powersetCard (#S - k), ∏ a ∈ T, (X - C a) := by


Suggested change

↑(k.factorial) * ∑ T ∈ S.powersetCard (#S - k), ∏ a ∈ T, (X - C a) := by

(k.factorial : R[X]) * ∑ T ∈ S.powersetCard (#S - k), ∏ a ∈ T, (X - C a) := by

Not sure what the point here is

YaelDillies · 2026-10-25T15:54:39Z

I don't mean that we should copy APIs into Polynomial namespace. I suggest that we should split these changes (removing APIs in Polynomial) into another PR.

This is what this PR used to do, but I realised that it felt incomplete not to remove the now-duplicated API. I can still split the PR up if you insist, but it would quite a bit of extra work for me to make the first PR good standalone.

mathlib-merge-conflicts · 2026-10-28T01:57:42Z

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

mathlib-merge-conflicts · 2026-10-28T17:44:59Z

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

github-actions Bot added the tech debt Fixes cross-cutting technical debt, see the "technical debt counters" stream on zulip label Jul 21, 2026

NoahW314 reviewed Jul 21, 2026

View reviewed changes

Comment thread Mathlib/Algebra/Polynomial/AlgebraMap.lean Outdated

Comment thread Mathlib/Algebra/Polynomial/Basic.lean Outdated

YaelDillies added t-algebra Algebra (groups, rings, fields, etc) LLM-generated PRs with substantial input from LLMs - review accordingly labels Jul 22, 2026

mathlib-merge-conflicts 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 17, 2026

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 Aug 20, 2026

mathlib-merge-conflicts 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 Sep 2, 2026

YaelDillies force-pushed the polynomial_abbrev branch from ac95901 to 60d3b4b Compare September 3, 2026 10:11

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 Sep 3, 2026

mathlib-merge-conflicts 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 Sep 9, 2026

YaelDillies force-pushed the polynomial_abbrev branch from c550ed8 to b918904 Compare September 11, 2026 10:58

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 Sep 11, 2026

mathlib-merge-conflicts 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 Sep 15, 2026

YaelDillies force-pushed the polynomial_abbrev branch from 9916043 to 433b882 Compare September 17, 2026 08:11

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 Sep 17, 2026

mathlib-merge-conflicts 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 Sep 26, 2026

YaelDillies force-pushed the polynomial_abbrev branch from 49b8db3 to bf2e0cb Compare September 26, 2026 13:48

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 Sep 26, 2026

mathlib-merge-conflicts 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 Sep 28, 2026

mathlib-merge-conflicts 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 Oct 7, 2026

YaelDillies added 3 commits October 8, 2026 12:21

delete some more Polynomial stuff

060d7d0

fix

76a1987

YaelDillies force-pushed the polynomial_abbrev branch from e57b899 to 76a1987 Compare October 8, 2026 10:21

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 Oct 8, 2026

mathlib-triage Bot assigned jjdishere Oct 13, 2026

mathlib-merge-conflicts 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 Oct 16, 2026

Merge remote-tracking branch 'origin/master' into polynomial_abbrev

b8c4cb1

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 Oct 16, 2026

fix

b287378

jjdishere reviewed Oct 24, 2026

View reviewed changes

jjdishere added the awaiting-author Reply -awaiting-author to remove the label on your PR once you have addressed all comments. label Oct 24, 2026

Jiedong's review

54c6ec8

YaelDillies removed the awaiting-author Reply -awaiting-author to remove the label on your PR once you have addressed all comments. label Oct 25, 2026

github-actions 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 Oct 25, 2026

YaelDillies added 2 commits October 25, 2026 17:03

deprecated aliases

1402172

Merge remote-tracking branch 'origin/master' into polynomial_abbrev

4ee2a23

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 Oct 25, 2026

mathlib-merge-conflicts 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 Oct 28, 2026

Merge remote-tracking branch 'origin/master' into polynomial_abbrev

652861b

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 Oct 28, 2026

mathlib-merge-conflicts 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 Oct 28, 2026

	↑(k.factorial) * ∑ T ∈ S.powersetCard (#S - k), ∏ a ∈ T, (X - C a) := by
	(k.factorial : R[X]) * ∑ T ∈ S.powersetCard (#S - k), ∏ a ∈ T, (X - C a) := by

Conversation

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

Uh oh!

Uh oh!

github-actions Bot commented Jul 21, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 652861bf80

Import changes for modified files

Declarations diff (regex)

Declarations diff (Lean -- stale, waiting for the new build)

Uh oh!

Uh oh!

Uh oh!

tb65536 commented Jul 23, 2026

Uh oh!

leanprover-radar commented Jul 23, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

tb65536 commented Jul 23, 2026

Uh oh!

YaelDillies commented Jul 24, 2026

Uh oh!

mathlib-merge-conflicts Bot commented Aug 17, 2026

Uh oh!

mathlib-merge-conflicts Bot commented Sep 2, 2026

Uh oh!

mathlib-merge-conflicts Bot commented Sep 9, 2026

Uh oh!

mathlib-merge-conflicts Bot commented Sep 15, 2026

Uh oh!

mathlib-merge-conflicts Bot commented Sep 26, 2026

Uh oh!

mathlib-merge-conflicts Bot commented Sep 28, 2026

Uh oh!

mathlib-merge-conflicts Bot commented Oct 7, 2026

Uh oh!

mathlib-merge-conflicts Bot commented Oct 16, 2026

Uh oh!

jjdishere commented Oct 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

jjdishere commented Oct 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

jjdishere left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

jjdishere Oct 24, 2026

Choose a reason for hiding this comment

Uh oh!

YaelDillies Oct 25, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

YaelDillies commented Oct 25, 2026

Uh oh!

mathlib-merge-conflicts Bot commented Oct 28, 2026

Uh oh!

mathlib-merge-conflicts Bot commented Oct 28, 2026

Uh oh!

This branch has not been deployed

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

YaelDillies commented Jul 21, 2026 •

edited

Loading

github-actions Bot commented Jul 21, 2026 •

edited

Loading

leanprover-radar commented Jul 23, 2026 •

edited

Loading

jjdishere commented Oct 24, 2026 •

edited

Loading

jjdishere commented Oct 24, 2026 •

edited

Loading