Commit 2025-01-23 12:19 cae01b30

View on Github →

feat(MvPolynomial): commuting the variables of mv-polynomials of mv-polynomials (#20447) From GrowthInGroups (LeanCamCombi)

Estimated changes

Modified Mathlib/Algebra/MvPolynomial/Equiv.lean

modified theorem MvPolynomial.aeval_injective_iff_of_isEmpty

added def MvPolynomial.commAlgEquiv

added theorem MvPolynomial.commAlgEquiv_C

added theorem MvPolynomial.commAlgEquiv_C_X

added theorem MvPolynomial.commAlgEquiv_X

modified def MvPolynomial.isEmptyAlgEquiv

modified def MvPolynomial.isEmptyRingEquiv

added theorem MvPolynomial.isEmptyRingEquiv_eq_coeff_zero

added theorem MvPolynomial.isEmptyRingEquiv_symm_apply

added theorem MvPolynomial.isEmptyRingEquiv_symm_toRingHom