Commit 2026-03-26 09:32 039a8fe1

View on Github →

refactor(Algebra/MvPolynomial): turn into an abbrev (#36678) There is no semantic difference between MvPolynomial and AddMonoidAlgebra. A multivariate polynomial is an element of some add monoid algebra, while eg an element of an add monoid algebra can be represented as a finitely supported function.

Estimated changes

Modified Mathlib/Algebra/MonoidAlgebra/Cardinal.lean

added theorem MonoidAlgebra.cardinalMk_eq_lift_of_fintype

added theorem MonoidAlgebra.cardinalMk_eq_max_lift_of_infinite'

added theorem MonoidAlgebra.cardinalMk_eq_max_lift_of_infinite

deleted theorem MonoidAlgebra.cardinalMk_lift_of_fintype

deleted theorem MonoidAlgebra.cardinalMk_lift_of_infinite'

deleted theorem MonoidAlgebra.cardinalMk_lift_of_infinite

Modified Mathlib/Algebra/MonoidAlgebra/Defs.lean

Modified Mathlib/Algebra/MvPolynomial/Basic.lean

deleted def MvPolynomial

Modified Mathlib/Algebra/MvPolynomial/Cardinal.lean

modified theorem MvPolynomial.cardinalMk_eq_lift

modified theorem MvPolynomial.cardinalMk_eq_max

modified theorem MvPolynomial.cardinalMk_le_max

modified theorem MvPolynomial.cardinalMk_le_max_lift

Modified Mathlib/Algebra/MvPolynomial/CommRing.lean

Modified Mathlib/Algebra/MvPolynomial/Eval.lean

Modified Mathlib/FieldTheory/SeparablyGenerated.lean

Modified Mathlib/LinearAlgebra/Matrix/Adjugate.lean

Modified Mathlib/RingTheory/Finiteness/Descent.lean

Modified Mathlib/RingTheory/MvPolynomial.lean

Modified Mathlib/RingTheory/MvPolynomial/Basic.lean

Modified Mathlib/RingTheory/Polynomial/IsIntegral.lean

Modified Mathlib/RingTheory/Polynomial/UniversalFactorizationRing.lean