Scaling the roots of a polynomial #
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
- scale_roots p s = ∑ (i : ℕ) in p.support, ⇑(polynomial.monomial i) ((p.coeff i) * s ^ (p.nat_degree - i))
@[simp]
theorem
coeff_scale_roots
{R : Type u_3}
[comm_ring R]
(p : R[X])
(s : R)
(i : ℕ) :
(scale_roots p s).coeff i = (p.coeff i) * s ^ (p.nat_degree - i)
theorem
coeff_scale_roots_nat_degree
{R : Type u_3}
[comm_ring R]
(p : R[X])
(s : R) :
(scale_roots p s).coeff p.nat_degree = p.leading_coeff
theorem
scale_roots_ne_zero
{R : Type u_3}
[comm_ring R]
{p : R[X]}
(hp : p ≠ 0)
(s : R) :
scale_roots p s ≠ 0
theorem
support_scale_roots_le
{R : Type u_3}
[comm_ring R]
(p : R[X])
(s : R) :
(scale_roots p s).support ≤ p.support
theorem
support_scale_roots_eq
{R : Type u_3}
[comm_ring R]
(p : R[X])
{s : R}
(hs : s ∈ R⁰) :
(scale_roots p s).support = p.support
@[simp]
theorem
degree_scale_roots
{R : Type u_3}
[comm_ring R]
(p : R[X])
{s : R} :
(scale_roots p s).degree = p.degree
@[simp]
theorem
nat_degree_scale_roots
{R : Type u_3}
[comm_ring R]
(p : R[X])
(s : R) :
(scale_roots p s).nat_degree = p.nat_degree
theorem
monic_scale_roots_iff
{R : Type u_3}
[comm_ring R]
{p : R[X]}
(s : R) :
(scale_roots p s).monic ↔ p.monic
theorem
scale_roots_eval₂_eq_zero
{R : Type u_3}
{S : Type u_4}
[comm_ring R]
[comm_ring S]
{p : S[X]}
(f : S →+* R)
{r : R}
{s : S}
(hr : polynomial.eval₂ f r p = 0) :
polynomial.eval₂ f ((⇑f s) * r) (scale_roots p s) = 0
theorem
scale_roots_aeval_eq_zero
{R : Type u_3}
{S : Type u_4}
[comm_ring R]
[comm_ring S]
[algebra S R]
{p : S[X]}
{r : R}
{s : S}
(hr : ⇑(polynomial.aeval r) p = 0) :
⇑(polynomial.aeval ((⇑(algebra_map S R) s) * r)) (scale_roots p s) = 0
theorem
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 : A[X]}
{f : A →+* K}
(hf : function.injective ⇑f)
{r s : A}
(hr : polynomial.eval₂ f (⇑f r / ⇑f s) p = 0)
(hs : s ∈ A⁰) :
polynomial.eval₂ f (⇑f r) (scale_roots p s) = 0
theorem
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 : A[X]}
{r s : A}
(hr : ⇑(polynomial.aeval (⇑(algebra_map A K) r / ⇑(algebra_map A K) s)) p = 0)
(hs : s ∈ A⁰) :
⇑(polynomial.aeval (⇑(algebra_map A K) r)) (scale_roots p s) = 0