Commit 2025-01-31 18:21 03ee3833

View on Github →

chore(Mathlib/RingTheory/MvPolynomial): rename MonomiaOrder.lCoeff to MonomialOrder.leadingCoeff (#21290) For coherence with other names in mathlib, we rename MonomialOrder.lCoeff to MonomialOrder.leadingCoeff.

Estimated changes

Modified Mathlib/RingTheory/MvPolynomial/Groebner.lean

modified theorem MonomialOrder.degree_reduce_lt

added def MonomialOrder.reduce

Modified Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean

added theorem MonomialOrder.isUnit_leadingCoeff

deleted def MonomialOrder.lCoeff

deleted theorem MonomialOrder.lCoeff_add_of_lt

deleted theorem MonomialOrder.lCoeff_eq_zero_iff

deleted theorem MonomialOrder.lCoeff_is_unit_iff

deleted theorem MonomialOrder.lCoeff_monomial

deleted theorem MonomialOrder.lCoeff_mul

deleted theorem MonomialOrder.lCoeff_mul_of_isRegular_left

deleted theorem MonomialOrder.lCoeff_mul_of_isRegular_right

deleted theorem MonomialOrder.lCoeff_ne_zero_iff

deleted theorem MonomialOrder.lCoeff_sub_of_lt

deleted theorem MonomialOrder.lCoeff_zero

added def MonomialOrder.leadingCoeff

added theorem MonomialOrder.leadingCoeff_add_of_lt

added theorem MonomialOrder.leadingCoeff_eq_zero_iff

added theorem MonomialOrder.leadingCoeff_monomial

added theorem MonomialOrder.leadingCoeff_mul

added theorem MonomialOrder.leadingCoeff_mul_of_isRegular_left

added theorem MonomialOrder.leadingCoeff_mul_of_isRegular_right

added theorem MonomialOrder.leadingCoeff_ne_zero_iff

added theorem MonomialOrder.leadingCoeff_sub_of_lt

added theorem MonomialOrder.leadingCoeff_zero