# Scaling the roots of a polynomial #

This file defines scaleRoots 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.

noncomputable def Polynomial.scaleRoots {R : Type u_1} [] (p : ) (s : R) :

scaleRoots p s is a polynomial with root r * s for each root r of p.

Equations
• p.scaleRoots s = p.support.sum fun (i : ) => (p.coeff i * s ^ (p.natDegree - i))
Instances For
@[simp]
theorem Polynomial.coeff_scaleRoots {R : Type u_1} [] (p : ) (s : R) (i : ) :
(p.scaleRoots s).coeff i = p.coeff i * s ^ (p.natDegree - i)
theorem Polynomial.coeff_scaleRoots_natDegree {R : Type u_1} [] (p : ) (s : R) :
@[simp]
theorem Polynomial.zero_scaleRoots {R : Type u_1} [] (s : R) :
theorem Polynomial.scaleRoots_ne_zero {R : Type u_1} [] {p : } (hp : p 0) (s : R) :
p.scaleRoots s 0
theorem Polynomial.support_scaleRoots_le {R : Type u_1} [] (p : ) (s : R) :
(p.scaleRoots s).support p.support
theorem Polynomial.support_scaleRoots_eq {R : Type u_1} [] (p : ) {s : R} (hs : ) :
(p.scaleRoots s).support = p.support
@[simp]
theorem Polynomial.degree_scaleRoots {R : Type u_1} [] (p : ) {s : R} :
(p.scaleRoots s).degree = p.degree
@[simp]
theorem Polynomial.natDegree_scaleRoots {R : Type u_1} [] (p : ) (s : R) :
(p.scaleRoots s).natDegree = p.natDegree
theorem Polynomial.monic_scaleRoots_iff {R : Type u_1} [] {p : } (s : R) :
(p.scaleRoots s).Monic p.Monic
theorem Polynomial.map_scaleRoots {R : Type u_1} {S : Type u_2} [] [] (p : ) (x : R) (f : R →+* S) (h : f p.leadingCoeff 0) :
Polynomial.map f (p.scaleRoots x) = ().scaleRoots (f x)
@[simp]
theorem Polynomial.scaleRoots_C {R : Type u_1} [] (r : R) (c : R) :
(Polynomial.C c).scaleRoots r = Polynomial.C c
@[simp]
theorem Polynomial.scaleRoots_one {R : Type u_1} [] (p : ) :
p.scaleRoots 1 = p
@[simp]
theorem Polynomial.scaleRoots_zero {R : Type u_1} [] (p : ) :
p.scaleRoots 0 = p.leadingCoeff Polynomial.X ^ p.natDegree
@[simp]
theorem Polynomial.one_scaleRoots {R : Type u_1} [] (r : R) :
theorem Polynomial.scaleRoots_eval₂_mul_of_commute {S : Type u_2} {A : Type u_3} [] [] {p : } (f : S →+* A) (a : A) (s : S) (hsa : Commute (f s) a) (hf : ∀ (s₁ s₂ : S), Commute (f s₁) (f s₂)) :
Polynomial.eval₂ f (f s * a) (p.scaleRoots s) = f s ^ p.natDegree *
theorem Polynomial.scaleRoots_eval₂_mul {R : Type u_1} {S : Type u_2} [] [] {p : } (f : S →+* R) (r : R) (s : S) :
Polynomial.eval₂ f (f s * r) (p.scaleRoots s) = f s ^ p.natDegree *
theorem Polynomial.scaleRoots_eval₂_eq_zero {R : Type u_1} {S : Type u_2} [] [] {p : } (f : S →+* R) {r : R} {s : S} (hr : = 0) :
Polynomial.eval₂ f (f s * r) (p.scaleRoots s) = 0
theorem Polynomial.scaleRoots_aeval_eq_zero {R : Type u_1} {A : Type u_3} [] [] [Algebra R A] {p : } {a : A} {r : R} (ha : () p = 0) :
(Polynomial.aeval (() r * a)) (p.scaleRoots r) = 0
theorem Polynomial.scaleRoots_eval₂_eq_zero_of_eval₂_div_eq_zero {S : Type u_2} {K : Type u_4} [] [] {p : } {f : S →+* K} (hf : ) {r : S} {s : S} (hr : Polynomial.eval₂ f (f r / f s) p = 0) (hs : ) :
Polynomial.eval₂ f (f r) (p.scaleRoots s) = 0
theorem Polynomial.scaleRoots_aeval_eq_zero_of_aeval_div_eq_zero {R : Type u_1} {K : Type u_4} [] [] [Algebra R K] (inj : Function.Injective ()) {p : } {r : R} {s : R} (hr : (Polynomial.aeval (() r / () s)) p = 0) (hs : ) :
(Polynomial.aeval (() r)) (p.scaleRoots s) = 0
@[simp]
theorem Polynomial.scaleRoots_mul {R : Type u_1} [] (p : ) (r : R) (s : R) :
p.scaleRoots (r * s) = (p.scaleRoots r).scaleRoots s
theorem Polynomial.mul_scaleRoots {R : Type u_1} [] (p : ) (q : ) (r : R) :
r ^ (p.natDegree + q.natDegree - (p * q).natDegree) (p * q).scaleRoots r = p.scaleRoots r * q.scaleRoots r

Multiplication and scaleRoots commute up to a power of r. The factor disappears if we assume that the product of the leading coeffs does not vanish. See Polynomial.mul_scaleRoots'.

theorem Polynomial.mul_scaleRoots' {R : Type u_1} [] (p : ) (q : ) (r : R) (h : p.leadingCoeff * q.leadingCoeff 0) :
(p * q).scaleRoots r = p.scaleRoots r * q.scaleRoots r
theorem Polynomial.mul_scaleRoots_of_noZeroDivisors {R : Type u_1} [] (p : ) (q : ) (r : R) [] :
(p * q).scaleRoots r = p.scaleRoots r * q.scaleRoots r
theorem Polynomial.add_scaleRoots_of_natDegree_eq {R : Type u_1} [] (p : ) (q : ) (r : R) (h : p.natDegree = q.natDegree) :
r ^ (p.natDegree - (p + q).natDegree) (p + q).scaleRoots r = p.scaleRoots r + q.scaleRoots r
theorem Polynomial.scaleRoots_dvd' {R : Type u_1} [] (p : ) (q : ) {r : R} (hr : ) (hpq : p q) :
p.scaleRoots r q.scaleRoots r
theorem Polynomial.scaleRoots_dvd {R : Type u_1} [] (p : ) (q : ) {r : R} [] (hpq : p q) :
p.scaleRoots r q.scaleRoots r
theorem Dvd.dvd.scaleRoots {R : Type u_1} [] (p : ) (q : ) {r : R} [] (hpq : p q) :
p.scaleRoots r q.scaleRoots r

Alias of Polynomial.scaleRoots_dvd.

theorem Polynomial.scaleRoots_dvd_iff {R : Type u_1} [] (p : ) (q : ) {r : R} (hr : ) :
p.scaleRoots r q.scaleRoots r p q
theorem IsUnit.scaleRoots_dvd_iff {R : Type u_1} [] (p : ) (q : ) {r : R} (hr : ) :
p.scaleRoots r q.scaleRoots r p q

Alias of Polynomial.scaleRoots_dvd_iff.

theorem Polynomial.isCoprime_scaleRoots {R : Type u_1} [] (p : ) (q : ) (r : R) (hr : ) (h : ) :
IsCoprime (p.scaleRoots r) (q.scaleRoots r)
theorem IsCoprime.scaleRoots {R : Type u_1} [] (p : ) (q : ) (r : R) (hr : ) (h : ) :
IsCoprime (p.scaleRoots r) (q.scaleRoots r)

Alias of Polynomial.isCoprime_scaleRoots.