Documentation

Mathlib.Algebra.Polynomial.Degree.Monomial

Degree of univariate monomials #

theorem Polynomial.natDegree_le_pred {R : Type u} {n : Nat} [Semiring R] {p : Polynomial R} (hf : LE.le p.natDegree n) (hn : Eq (p.coeff n) 0) :