Theorem MonomialOrder.mem_nonZeroDivisors_of_leadingCoeff_mem_nonZeroDivisors

Modification history

2026-03-30 13:40
Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
feat(RingTheory/MvPolynomial/MonomialOrder): misc lemmas (#34758)
Added MonomialOrder.mem_nonZeroDivisors_of_leadingCoeff_mem_nonZeroDivisorsView on Github →