16.2. Degree
16.2.1. natDegree versus degree
Mathlib provides two notions of degree, differing only in how they treat the zero polynomial:
#check (natDegree : R[X] → ℕ)
#check (degree : R[X] → WithBot ℕ)
For non-zero polynomials the two agree (via the coercion ((↑·) : ℕ → WithBot ℕ));
see Polynomial.degree_eq_natDegree.
They differ at the zero polynomial: Polynomial.natDegree_zero gives
(0 : R[X]).natDegree = 0, while Polynomial.degree_zero gives
(0 : R[X]).degree = ⊥.
Many statements exist in both degree and natDegree form.
Sometimes, using degree lets you deal uniformly with exceptions around the polynomial 0.
Other times, viewing the polynomial 0 as a constant is exactly what is needed.
Another important distinction is that natDegree takes values in ℕ,
where more tactics are likely to help close goals.
Coverage of both spellings is generally good, but in practice it varies lemma by lemma:
if the form you want is missing, look for it under the other name,
or use Polynomial.degree_eq_natDegree to convert between them.
For computing or bounding the degree of a concrete polynomial built from C,
X and ring operations, the compute_degree tactic
(and its stronger variant compute_degree!) is often the easiest tool:
example : (X ^ 3 + C 2 * X + 1 : R[X]).natDegree ≤ 3 := R:Type u_1inst✝:Semiring R⊢ (X ^ 3 + C 2 * X + 1).natDegree ≤ 3
All goals completed! 🐙
16.2.2. Leading coefficient and monic polynomials
The Polynomial.leadingCoeff of p is its coefficient at degree p.natDegree:
example : R := p.leadingCoeff
example : p.leadingCoeff = p.coeff p.natDegree := rfl
A polynomial is monic if its leading coefficient is 1.
The predicate is Polynomial.Monic, defined as exactly this equality;
the named unfolding lemma is Polynomial.Monic.def:
example : p.Monic ↔ p.leadingCoeff = 1 := Monic.def
Common building blocks include Polynomial.monic_one, Polynomial.monic_X_add_C
and Polynomial.monic_X_sub_C, and Polynomial.Monic.mul
shows that monicity is preserved by multiplication.