Theorem MvPolynomial.dvd_smul_X_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_smul_X_iff_existsView on Github →
2025-12-22 09:02
Mathlib/RingTheory/MvPolynomial/MonomialOrder/DegLex.lean
feat(RingTheory/MvPolynomial/IrrQuadratic): irreducibility of sum X_i Y_i (#31161) …
Added MvPolynomial.dvd_smul_X_iff_existsView on Github →