Theorem MvPolynomial.totalDegree_le_of_dvd_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_le_of_dvd_of_isDomainView on Github →
2025-12-01 17:55
Mathlib/RingTheory/MvPolynomial/MonomialOrder/DegLex.lean
feat: divisibility lemmas for multivariate polynomials (#32226) …
Added MvPolynomial.totalDegree_le_of_dvd_of_isDomainView on Github →