Theorem MvPolynomial.isHomogeneous_of_totalDegree_zero

Modification history

2024-04-15 15:25

Mathlib/RingTheory/MvPolynomial/Homogeneous.lean

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

Deleted MvPolynomial.isHomogeneous_of_totalDegree_zero View on Github →

2023-05-20 10:39

Mathlib/RingTheory/MvPolynomial/Homogeneous.lean

feat: port RingTheory.MvPolynomial.Homogeneous (#4138)

Added MvPolynomial.isHomogeneous_of_totalDegree_zero View on Github →