Theory of univariate polynomials #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
The main defs here are eval₂
, eval
, and map
.
We give several lemmas about their interaction with each other and with module operations.
Evaluate a polynomial p
given a ring hom f
from the scalar ring
to the target and a value x
for the variable in the target
eval₂_add_monoid_hom (f : R →+* S) (x : S)
is the add_monoid_hom
from
R[X]
to S
obtained by evaluating the pushforward of p
along f
at x
.
Equations
- polynomial.eval₂_add_monoid_hom f x = {to_fun := polynomial.eval₂ f x, map_zero' := _, map_add' := _}
eval₂
as a ring_hom
for noncommutative rings
Equations
- polynomial.eval₂_ring_hom' f x hf = {to_fun := polynomial.eval₂ f x, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
We next prove that eval₂ is multiplicative as long as target ring is commutative (even if the source ring is not).
eval₂
as a ring_hom
Equations
- polynomial.eval₂_ring_hom f x = {to_fun := (polynomial.eval₂_add_monoid_hom f x).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
eval x p
is the evaluation of the polynomial p
at x
Equations
A reformulation of the expansion of (1 + y)^d: $$(d + 1) (1 + y)^d - (d + 1)y^d = \sum_{i = 0}^d {d + 1 \choose i} \cdot i \cdot y^{i - 1}.$$
polynomial.eval
as linear map
Equations
- polynomial.leval r = {to_fun := λ (f : polynomial R), polynomial.eval r f, map_add' := _, map_smul' := _}
is_root p x
implies x
is a root of p
. The evaluation of p
at x
is zero
Equations
- p.is_root a = (polynomial.eval a p = 0)
Instances for polynomial.is_root
Equations
- polynomial.is_root.decidable = polynomial.is_root.decidable._proof_1.mpr (_inst_2 (polynomial.eval a p) 0)
The composition of polynomials as a polynomial.
Equations
- p.comp q = polynomial.eval₂ polynomial.C q p
map f p
maps a polynomial p
across a ring hom f
Equations
Instances for polynomial.map
polynomial.map
as a ring_hom
.
Equations
- polynomial.map_ring_hom f = {to_fun := polynomial.map f, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
If R
and S
are isomorphic, then so are their polynomial rings.
Equations
we have made eval₂
irreducible from the start.
Perhaps we can make also eval
, comp
, and map
irreducible too?
eval r
, regarded as a ring homomorphism from R[X]
to R
.
Equations
comp p
, regarded as a ring homomorphism from R[X]
to itself.
Polynomial evaluation commutes with list.prod
Polynomial evaluation commutes with multiset.prod
Polynomial evaluation commutes with finset.prod