Theorem MonomialOrder.sPolynomial_lt_of_degree_ne_zero_of_degree_eq

Modification history

2025-12-04 18:52
Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
feat(RingTheory/MvPolynomial/MonomialOrder): add S-polynomial (#32344) …
Added MonomialOrder.sPolynomial_lt_of_degree_ne_zero_of_degree_eqView on Github →