Commit 2026-03-30 13:40 f98299e3

View on Github →

feat(RingTheory/MvPolynomial/MonomialOrder): misc lemmas (#34758)

Estimated changes

Modified Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean

added theorem MonomialOrder.degree_le_degree_of_support_subset

added theorem MonomialOrder.le_degree_of_mem_support

added theorem MonomialOrder.leadingTerm_eq_leadingTerm_iff

added theorem MonomialOrder.mem_nonZeroDivisors_of_leadingCoeff_mem_nonZeroDivisors

added theorem MonomialOrder.monic_C_one

added theorem MonomialOrder.monic_leadingTerm

added theorem MonomialOrder.monic_of_subsingleton

modified theorem MonomialOrder.monic_one

added theorem MonomialOrder.support_leadingTerm'

added theorem MonomialOrder.support_leadingTerm

added theorem MonomialOrder.toSyn_degree_mul_le