Theorem MonomialOrder.coeff_sPolynomial_sup_eq_zero

Modification history

2025-12-04 18:52

Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean

feat(RingTheory/MvPolynomial/MonomialOrder): add S-polynomial (#32344) …

Added MonomialOrder.coeff_sPolynomial_sup_eq_zero View on Github →