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} [Semiring R] (p : Polynomial R) (s : R) : Polynomial R

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

Equations

• Polynomial.scaleRoots p s = Finset.sum (Polynomial.support p) fun i => ↑(Polynomial.monomial i) (Polynomial.coeff p i * s ^ (Polynomial.natDegree p - i))

@[simp]

theorem Polynomial.coeff_scaleRoots {R : Type u_1} [Semiring R] (p : Polynomial R) (s : R) (i : ℕ) : Polynomial.coeff (Polynomial.scaleRoots p s) i = Polynomial.coeff p i * s ^ (Polynomial.natDegree p - i)

theorem Polynomial.coeff_scaleRoots_natDegree {R : Type u_1} [Semiring R] (p : Polynomial R) (s : R) : Polynomial.coeff (Polynomial.scaleRoots p s) (Polynomial.natDegree p) = Polynomial.leadingCoeff p

@[simp]

theorem Polynomial.zero_scaleRoots {R : Type u_1} [Semiring R] (s : R) : Polynomial.scaleRoots 0 s = 0

theorem Polynomial.scaleRoots_ne_zero {R : Type u_1} [Semiring R] {p : Polynomial R} (hp : p ≠ 0) (s : R) : Polynomial.scaleRoots p s ≠ 0

theorem Polynomial.support_scaleRoots_le {R : Type u_1} [Semiring R] (p : Polynomial R) (s : R) : Polynomial.support (Polynomial.scaleRoots p s) ≤ Polynomial.support p

theorem Polynomial.support_scaleRoots_eq {R : Type u_1} [Semiring R] (p : Polynomial R) {s : R} (hs : s ∈ nonZeroDivisors R) : Polynomial.support (Polynomial.scaleRoots p s) = Polynomial.support p

@[simp]

theorem Polynomial.degree_scaleRoots {R : Type u_1} [Semiring R] (p : Polynomial R) {s : R} : Polynomial.degree (Polynomial.scaleRoots p s) = Polynomial.degree p

@[simp]

theorem Polynomial.natDegree_scaleRoots {R : Type u_1} [Semiring R] (p : Polynomial R) (s : R) : Polynomial.natDegree (Polynomial.scaleRoots p s) = Polynomial.natDegree p

theorem Polynomial.monic_scaleRoots_iff {R : Type u_1} [Semiring R] {p : Polynomial R} (s : R) : Polynomial.Monic (Polynomial.scaleRoots p s) ↔ Polynomial.Monic p

theorem Polynomial.map_scaleRoots {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (p : Polynomial R) (x : R) (f : R →+* S) (h : ↑f (Polynomial.leadingCoeff p) ≠ 0) : Polynomial.map f (Polynomial.scaleRoots p x) = Polynomial.scaleRoots (Polynomial.map f p) (↑f x)

theorem Polynomial.scaleRoots_eval₂_mul {R : Type u_1} {S : Type u_2} [Semiring S] [CommSemiring R] {p : Polynomial S} (f : S →+* R) (r : R) (s : S) : Polynomial.eval₂ f (↑f s * r) (Polynomial.scaleRoots p s) = ↑f s ^ Polynomial.natDegree p * Polynomial.eval₂ f r p

theorem Polynomial.scaleRoots_eval₂_eq_zero {R : Type u_1} {S : Type u_2} [Semiring S] [CommSemiring R] {p : Polynomial S} (f : S →+* R) {r : R} {s : S} (hr : Polynomial.eval₂ f r p = 0) : Polynomial.eval₂ f (↑f s * r) (Polynomial.scaleRoots p s) = 0

theorem Polynomial.scaleRoots_aeval_eq_zero {R : Type u_1} {A : Type u_3} [CommSemiring R] [CommSemiring A] [Algebra R A] {p : Polynomial R} {a : A} {r : R} (ha : ↑(Polynomial.aeval a) p = 0) : ↑(Polynomial.aeval (↑(algebraMap R A) r * a)) (Polynomial.scaleRoots p r) = 0

theorem Polynomial.scaleRoots_eval₂_eq_zero_of_eval₂_div_eq_zero {S : Type u_2} {K : Type u_4} [Semiring S] [Field K] {p : Polynomial S} {f : S →+* K} (hf : Function.Injective ↑f) {r : S} {s : S} (hr : Polynomial.eval₂ f (↑f r / ↑f s) p = 0) (hs : s ∈ nonZeroDivisors S) : Polynomial.eval₂ f (↑f r) (Polynomial.scaleRoots p s) = 0

theorem Polynomial.scaleRoots_aeval_eq_zero_of_aeval_div_eq_zero {R : Type u_1} {K : Type u_4} [CommSemiring R] [Field K] [Algebra R K] (inj : Function.Injective ↑(algebraMap R K)) {p : Polynomial R} {r : R} {s : R} (hr : ↑(Polynomial.aeval (↑(algebraMap R K) r / ↑(algebraMap R K) s)) p = 0) (hs : s ∈ nonZeroDivisors R) : ↑(Polynomial.aeval (↑(algebraMap R K) r)) (Polynomial.scaleRoots p s) = 0