Theorems · Theorem · commutative algebra

MonomialOrder.coeff_mul_of_add_of_degree_le

∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {f g : MvPolynomial σ R} {a b : σ →₀ ℕ},
  m.toSyn (m.degree f) ≤ m.toSyn a →
    m.toSyn (m.degree g) ≤ m.toSyn b →
      MvPolynomial.coeff (a + b) (f * g) = MvPolynomial.coeff a f * MvPolynomial.coeff b g

Multiplicativity of leading coefficients

Defined in

Mathlib.RingTheory.MvPolynomial.MonomialOrder

Cited by

3 results in Mathlib

Foundations

Depth 87 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiring