Commit 2026-04-07 10:49 95f52ba7

View on Github →

refactor(Algebra/MvPolynomial): redefine map in terms of AddMonoidAlgebra (#37210) This is a step towards unifying MvPolynomial and AddMonoidAlgebra and making the latter a structure.

Estimated changes

Modified Mathlib/Algebra/MonoidAlgebra/Basic.lean

added theorem MonoidAlgebra.mapAlgEquiv_trans

deleted theorem MonoidAlgebra.mapRangeAlgEquiv_trans

modified theorem MonoidAlgebra.symm_mapAlgEquiv

Modified Mathlib/Algebra/MvPolynomial/Basic.lean

added theorem MvPolynomial.coeff_addMonoidAlgebraMap

deleted theorem MvPolynomial.coeff_mapRange

Modified Mathlib/Algebra/MvPolynomial/Equiv.lean

added theorem MvPolynomial.mapAlgEquiv_apply

added theorem MvPolynomial.mapEquiv_apply

Modified Mathlib/Algebra/MvPolynomial/Eval.lean

modified def MvPolynomial.map

added theorem MvPolynomial.mapAlgHom_apply

modified theorem MvPolynomial.map_X

added theorem MvPolynomial.map_eq_eval₂Hom_C_comp

modified theorem MvPolynomial.map_id

Modified Mathlib/Algebra/MvPolynomial/Rename.lean

Modified Mathlib/LinearAlgebra/Matrix/Charpoly/Univ.lean

Modified Mathlib/RingTheory/MvPolynomial/Homogeneous.lean

deleted theorem MvPolynomial.IsHomogeneous.map

Modified Mathlib/RingTheory/MvPowerSeries/Expand.lean

Modified Mathlib/RingTheory/Polynomial/UniversalFactorizationRing.lean

Modified Mathlib/RingTheory/Smooth/Basic.lean

Modified Mathlib/RingTheory/Smooth/IntegralClosure.lean

Modified Mathlib/RingTheory/TensorProduct/MvPolynomial.lean