Commit 2025-02-20 08:28 762900d5

View on Github →

feat(RingTheory/MvPolynomial/MonomialOrder/Monic): monic polynomials wrt a monomial order (#21546)

Estimated changes

Modified Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean

added theorem MonomialOrder.Monic.add_of_lt

added theorem MonomialOrder.Monic.coeff_degree

added theorem MonomialOrder.Monic.leadingCoeff_eq_one

added theorem MonomialOrder.Monic.mul

added theorem MonomialOrder.Monic.ne_zero

added theorem MonomialOrder.Monic.of_subsingleton

added def MonomialOrder.Monic

added theorem MonomialOrder.coeff_pow_nsmul_degree

modified def MonomialOrder.degree

added theorem MonomialOrder.degree_X_add_C

added theorem MonomialOrder.degree_X_sub_C

added theorem MonomialOrder.degree_mul_of_mul_leadingCoeff_ne_zero

deleted theorem MonomialOrder.degree_mul_of_nonzero_mul

added theorem MonomialOrder.degree_one

added theorem MonomialOrder.degree_pow

added theorem MonomialOrder.degree_pow_le

added theorem MonomialOrder.degree_pow_of_pow_leadingCoeff_ne_zero

added theorem MonomialOrder.degree_subsingleton

modified def MonomialOrder.leadingCoeff

added theorem MonomialOrder.leadingCoeff_X

modified theorem MonomialOrder.leadingCoeff_mul

added theorem MonomialOrder.leadingCoeff_mul_of_mul_leadingCoeff_ne_zero

added theorem MonomialOrder.leadingCoeff_neg

added theorem MonomialOrder.leadingCoeff_one

added theorem MonomialOrder.leadingCoeff_pow

added theorem MonomialOrder.leadingCoeff_pow_of_pow_leadingCoeff_ne_zero

added theorem MonomialOrder.monic_X

added theorem MonomialOrder.monic_X_add_C

added theorem MonomialOrder.monic_X_sub_C

added theorem MonomialOrder.monic_monomial

added theorem MonomialOrder.monic_monomial_one

added theorem MonomialOrder.monic_one