Scaling the roots of a polynomial #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file defines scale_roots p s for a polynomial p in one variable and a ring element s to
be the polynomial with root r * s for each root r of p and proves some basic results about it.
scale_roots p s is a polynomial with root r * s for each root r of p.
Equations
- p.scale_roots s = p.support.sum (λ (i : ℕ), ⇑(polynomial.monomial i) (p.coeff i * s ^ (p.nat_degree - i)))
@[simp]
theorem
polynomial.coeff_scale_roots
{R : Type u_3}
[comm_ring R]
(p : polynomial R)
(s : R)
(i : ℕ) :
(p.scale_roots s).coeff i = p.coeff i * s ^ (p.nat_degree - i)
theorem
polynomial.coeff_scale_roots_nat_degree
{R : Type u_3}
[comm_ring R]
(p : polynomial R)
(s : R) :
(p.scale_roots s).coeff p.nat_degree = p.leading_coeff
@[simp]
theorem
polynomial.scale_roots_ne_zero
{R : Type u_3}
[comm_ring R]
{p : polynomial R}
(hp : p ≠ 0)
(s : R) :
p.scale_roots s ≠ 0
theorem
polynomial.support_scale_roots_le
{R : Type u_3}
[comm_ring R]
(p : polynomial R)
(s : R) :
(p.scale_roots s).support ≤ p.support
theorem
polynomial.support_scale_roots_eq
{R : Type u_3}
[comm_ring R]
(p : polynomial R)
{s : R}
(hs : s ∈ non_zero_divisors R) :
(p.scale_roots s).support = p.support
@[simp]
theorem
polynomial.degree_scale_roots
{R : Type u_3}
[comm_ring R]
(p : polynomial R)
{s : R} :
(p.scale_roots s).degree = p.degree
@[simp]
theorem
polynomial.nat_degree_scale_roots
{R : Type u_3}
[comm_ring R]
(p : polynomial R)
(s : R) :
(p.scale_roots s).nat_degree = p.nat_degree
theorem
polynomial.monic_scale_roots_iff
{R : Type u_3}
[comm_ring R]
{p : polynomial R}
(s : R) :
(p.scale_roots s).monic ↔ p.monic
theorem
polynomial.scale_roots_eval₂_mul
{R : Type u_3}
{S : Type u_4}
[comm_ring R]
[comm_ring S]
{p : polynomial S}
(f : S →+* R)
(r : R)
(s : S) :
polynomial.eval₂ f (⇑f s * r) (p.scale_roots s) = ⇑f s ^ p.nat_degree * polynomial.eval₂ f r p
theorem
polynomial.scale_roots_eval₂_eq_zero
{R : Type u_3}
{S : Type u_4}
[comm_ring R]
[comm_ring S]
{p : polynomial S}
(f : S →+* R)
{r : R}
{s : S}
(hr : polynomial.eval₂ f r p = 0) :
polynomial.eval₂ f (⇑f s * r) (p.scale_roots s) = 0
theorem
polynomial.scale_roots_aeval_eq_zero
{R : Type u_3}
{S : Type u_4}
[comm_ring R]
[comm_ring S]
[algebra S R]
{p : polynomial S}
{r : R}
{s : S}
(hr : ⇑(polynomial.aeval r) p = 0) :
⇑(polynomial.aeval (⇑(algebra_map S R) s * r)) (p.scale_roots s) = 0
theorem
polynomial.scale_roots_eval₂_eq_zero_of_eval₂_div_eq_zero
{A : Type u_1}
{K : Type u_2}
[comm_ring A]
[is_domain A]
[field K]
{p : polynomial A}
{f : A →+* K}
(hf : function.injective ⇑f)
{r s : A}
(hr : polynomial.eval₂ f (⇑f r / ⇑f s) p = 0)
(hs : s ∈ non_zero_divisors A) :
polynomial.eval₂ f (⇑f r) (p.scale_roots s) = 0
theorem
polynomial.scale_roots_aeval_eq_zero_of_aeval_div_eq_zero
{A : Type u_1}
{K : Type u_2}
[comm_ring A]
[is_domain A]
[field K]
[algebra A K]
(inj : function.injective ⇑(algebra_map A K))
{p : polynomial A}
{r s : A}
(hr : ⇑(polynomial.aeval (⇑(algebra_map A K) r / ⇑(algebra_map A K) s)) p = 0)
(hs : s ∈ non_zero_divisors A) :
⇑(polynomial.aeval (⇑(algebra_map A K) r)) (p.scale_roots s) = 0
theorem
polynomial.map_scale_roots
{R : Type u_3}
{S : Type u_4}
[comm_ring R]
[comm_ring S]
(p : polynomial R)
(x : R)
(f : R →+* S)
(h : ⇑f p.leading_coeff ≠ 0) :
polynomial.map f (p.scale_roots x) = (polynomial.map f p).scale_roots (⇑f x)