Theorem MvPolynomial.totalDegree_zero_iff_isHomogeneous

Modification history

2024-04-15 15:25

Mathlib/RingTheory/MvPolynomial/Homogeneous.lean

refactor(RingTheory.MvPolynomial.Homogeneous): refactor in terms of weightedHomogeneous (#7609) …

Added MvPolynomial.totalDegree_zero_iff_isHomogeneous View on Github →