Theorem MonomialOrder.leadingCoeff_mul

Modification history

2026-02-09 11:44
Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
feat(RingTheory/MvPolynomial/MonomialOrder): remove unnecessary hypotheses of `leadingCoeff_mul` (#34765) …
Modified MonomialOrder.leadingCoeff_mulView on Github →
2025-12-10 17:42
Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
chore(RingTheory/MvPolynomial): weaken IsCancelMulZero to NoZeroDivisors in `degree_mul` and related lemmas. (#32558) …
Modified MonomialOrder.leadingCoeff_mulView on Github →
2025-04-08 21:08
Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
feat: generalize half of Mathlib.RingTheory (#23173) …
Modified MonomialOrder.leadingCoeff_mulView on Github →
2025-02-20 08:28
Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
feat(RingTheory/MvPolynomial/MonomialOrder/Monic): monic polynomials wrt a monomial order (#21546)
Modified MonomialOrder.leadingCoeff_mulView on Github →
2025-01-31 18:21
Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
chore(Mathlib/RingTheory/MvPolynomial): rename MonomiaOrder.lCoeff to MonomialOrder.leadingCoeff (#21290) …
Added MonomialOrder.leadingCoeff_mulView on Github →