Theorem MvPolynomial.dvd_monomial_one_iff_exists

Modification history

2026-01-03 10:56
Mathlib/Algebra/MvPolynomial/NoZeroDivisors.lean
feat: file for lemmas about MvPolynomials over NoZeroDivisors (#25925) …
Modified MvPolynomial.dvd_monomial_one_iff_existsView on Github →
2025-12-01 17:55
Mathlib/RingTheory/MvPolynomial/MonomialOrder/DegLex.lean
feat: divisibility lemmas for multivariate polynomials (#32226) …
Added MvPolynomial.dvd_monomial_one_iff_existsView on Github →