Theory of univariate polynomials #
The definitions include
degree
, monic
, leading_coeff
Results include
degree_mul
: The degree of the product is the sum of degreesleading_coeff_add_of_degree_eq
andleading_coeff_add_of_degree_lt
: The leading_coefficient of a sum is determined by the leading coefficients and degrees
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 = ⊥
.
Equations
- polynomial.has_well_founded = {r := λ (p q : polynomial R), p.degree < q.degree, wf := _}
nat_degree p
forces degree p
to ℕ, by defining nat_degree 0 = 0.
Equations
- p.nat_degree = option.get_or_else p.degree 0
leading_coeff p
gives the coefficient of the highest power of X
in p
Equations
- p.leading_coeff = p.coeff p.nat_degree
a polynomial is monic
if its leading coefficient is 1
Equations
- p.monic = (p.leading_coeff = 1)
Instances for polynomial.monic
Equations
- polynomial.monic.decidable = polynomial.monic.decidable._proof_1.mpr (_inst_2 p.leading_coeff 1)
Alias of the forward direction of polynomial.nat_degree_le_iff_degree_le
.
Alias of the reverse direction of polynomial.nat_degree_le_iff_degree_le
.
We can reexpress a sum over p.support
as a sum over range n
,
for any n
satisfying p.nat_degree < n
.
We can reexpress a sum over p.support
as a sum over range (p.nat_degree + 1)
.
The second-highest coefficient, or 0 for constants
Equations
- p.next_coeff = ite (p.nat_degree = 0) 0 (p.coeff (p.nat_degree - 1))
degree
as a monoid homomorphism between R[X]
and multiplicative (with_bot ℕ)
.
This is useful to prove results about multiplication and degree.
Equations
- polynomial.degree_monoid_hom = {to_fun := polynomial.degree _inst_1, map_one' := _, map_mul' := _}
polynomial.leading_coeff
bundled as a monoid_hom
when R
has no_zero_divisors
, and thus
leading_coeff
is multiplicative
Equations
- polynomial.leading_coeff_hom = {to_fun := polynomial.leading_coeff _inst_1, map_one' := _, map_mul' := _}