Theorems · Definition · field theory

Polynomial.degree

{R : Type u} → [inst : Semiring R] → Polynomial R → WithBot ℕ

degree p is the degree of the polynomial p, i.e. the largest X-exponent in p. degree p = some n when p ≠ 0 and n is the highest power of X that appears in p, otherwise degree 0 = ⊥.

Defined in

Mathlib.Algebra.Polynomial.Degree.Defs

Cited by

643 results in Mathlib

Foundations

Depth 24 from the axioms, rests on 341 definitions · uses propext, Quot.sound

Assumes

Semiring