Theorem MvPolynomial.isUnit_iff_totalDegree_of_isReduced

Modification history

2025-06-13 08:21
Mathlib/Algebra/MvPolynomial/Nilpotent.lean
feat(Algebra/MvPolynomial): nilpotents and units (#25062)
Added MvPolynomial.isUnit_iff_totalDegree_of_isReducedView on Github →