Theorem MvPolynomial.totalDegree_mul_of_isDomain

Modification history

2026-01-03 10:56
Mathlib/Algebra/MvPolynomial/NoZeroDivisors.lean
feat: file for lemmas about MvPolynomials over NoZeroDivisors (#25925) …
Modified MvPolynomial.totalDegree_mul_of_isDomainView on Github →
2025-12-01 17:55
Mathlib/RingTheory/MvPolynomial/MonomialOrder/DegLex.lean
feat: divisibility lemmas for multivariate polynomials (#32226) …
Modified MvPolynomial.totalDegree_mul_of_isDomainView on Github →
2025-05-05 11:25
Mathlib/RingTheory/MvPolynomial/MonomialOrder/DegLex.lean
feat(MvPolynomial): multiplicativity of `totalDegree` over domains (#24347)
Added MvPolynomial.totalDegree_mul_of_isDomainView on Github →