Theorems · Theorem · commutative algebra

MonomialOrder.degree_monomial

∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {d : σ →₀ ℕ} (c : R)
  [inst_1 : Decidable (c = 0)], m.degree ((MvPolynomial.monomial d) c) = if c = 0 then 0 else d

Defined in

Mathlib.RingTheory.MvPolynomial.MonomialOrder

Cited by

12 results in Mathlib

Foundations

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

Assumes

CommSemiringDecidable