Theorems · Theorem · commutative algebra

MonomialOrder.degree_prod

∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] [NoZeroDivisors R] {ι : Type u_3}
  {P : ι → MvPolynomial σ R} {s : Finset ι}, (∀ i ∈ s, P i ≠ 0) → m.degree (∏ i ∈ s, P i) = ∑ i ∈ s, m.degree (P i)

Defined in

Mathlib.RingTheory.MvPolynomial.MonomialOrder

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommSemiringNoZeroDivisors