Commit 2025-12-04 18:52 28417667

View on Github →

feat(RingTheory/MvPolynomial/MonomialOrder): add S-polynomial (#32344) It is used in the statement and proof of Buchberger's criterion. Co-authored-By: Hao Shen 3118181069@qq.com

Estimated changes

Modified Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean

added theorem MonomialOrder.coeff_sPolynomial_sup_eq_zero

added theorem MonomialOrder.degree_sPolynomial

added theorem MonomialOrder.degree_sPolynomial_le

added theorem MonomialOrder.degree_sPolynomial_lt_sup_degree

added theorem MonomialOrder.sPolynomial_antisymm

added theorem MonomialOrder.sPolynomial_decomposition'

added theorem MonomialOrder.sPolynomial_decomposition

added theorem MonomialOrder.sPolynomial_def

added theorem MonomialOrder.sPolynomial_left_zero

added theorem MonomialOrder.sPolynomial_lt_of_degree_ne_zero_of_degree_eq

added theorem MonomialOrder.sPolynomial_mul_monomial

added theorem MonomialOrder.sPolynomial_right_zero

added theorem MonomialOrder.sPolynomial_self