Theorems · Definition · commutative algebra

MonomialOrder.withBotDegree

{σ : Type u_1} → MonomialOrder σ → {R : Type u_2} → [inst : CommSemiring R] → MvPolynomial σ R → WithBot (σ →₀ ℕ)

the degree of a multivariate polynomial with respect to a monomial ordering, where polynomial 0 has degree ⊥, which is not equal to 0. MonomialOrder.withBotDegree is to MonomialOrder.degree as Polynomial.degree is to Polynomial.natDegree.

Defined in

Mathlib.RingTheory.MvPolynomial.MonomialOrder

Cited by

26 results in Mathlib

Foundations

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

Assumes

CommSemiring