Commit 2025-06-13 08:21 af9ecce9

View on Github →

feat(Algebra/MvPolynomial): nilpotents and units (#25062)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/MvPolynomial/Nilpotent.lean

added theorem MvPolynomial.isNilpotent_iff

added theorem MvPolynomial.isUnit_iff

added theorem MvPolynomial.isUnit_iff_eq_C_of_isReduced

added theorem MvPolynomial.isUnit_iff_totalDegree_of_isReduced

Modified Mathlib/Data/Finsupp/Basic.lean

added theorem Finsupp.embDomain_some_some

added def Finsupp.optionEquiv

added theorem Finsupp.some_update_none