# 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.

source
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

- p.scaleRoots s = ∑ i ∈ p.support, (Polynomial.monomial i) (p.coeff i * s ^ (p.natDegree - i))

Instances For

source
@[simp]
theorem Polynomial.coeff_scaleRoots {R : Type u_1} [Semiring R] (p : Polynomial R) (s : R) (i : ℕ) :
(p.scaleRoots s).coeff i = p.coeff i * s ^ (p.natDegree - i)
source
theorem Polynomial.coeff_scaleRoots_natDegree {R : Type u_1} [Semiring R] (p : Polynomial R) (s : R) :
(p.scaleRoots s).coeff p.natDegree = p.leadingCoeff
source
@[simp]
theorem Polynomial.zero_scaleRoots {R : Type u_1} [Semiring R] (s : R) :
scaleRoots 0 s = 0
source
theorem Polynomial.scaleRoots_ne_zero {R : Type u_1} [Semiring R] {p : Polynomial R} (hp : p ≠ 0) (s : R) :
p.scaleRoots s ≠ 0
source
theorem Polynomial.support_scaleRoots_le {R : Type u_1} [Semiring R] (p : Polynomial R) (s : R) :
(p.scaleRoots s).support ≤ p.support
source
theorem Polynomial.support_scaleRoots_eq {R : Type u_1} [Semiring R] (p : Polynomial R) {s : R} (hs : s ∈ nonZeroDivisors R) :
(p.scaleRoots s).support = p.support
source
@[simp]
theorem Polynomial.degree_scaleRoots {R : Type u_1} [Semiring R] (p : Polynomial R) {s : R} :
(p.scaleRoots s).degree = p.degree
source
@[simp]
theorem Polynomial.natDegree_scaleRoots {R : Type u_1} [Semiring R] (p : Polynomial R) (s : R) :
(p.scaleRoots s).natDegree = p.natDegree
source
theorem Polynomial.monic_scaleRoots_iff {R : Type u_1} [Semiring R] {p : Polynomial R} (s : R) :
(p.scaleRoots s).Monic ↔ p.Monic
source
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 p.leadingCoeff ≠ 0) :
map f (p.scaleRoots x) = (map f p).scaleRoots (f x)
source
@[simp]
theorem Polynomial.scaleRoots_C {R : Type u_1} [Semiring R] (r c : R) :
(C c).scaleRoots r = C c
source
@[simp]
theorem Polynomial.scaleRoots_one {R : Type u_1} [Semiring R] (p : Polynomial R) :
p.scaleRoots 1 = p
source
@[simp]
theorem Polynomial.scaleRoots_zero {R : Type u_1} [Semiring R] (p : Polynomial R) :
p.scaleRoots 0 = p.leadingCoeff • X ^ p.natDegree
source
@[simp]
theorem Polynomial.one_scaleRoots {R : Type u_1} [Semiring R] (r : R) :
scaleRoots 1 r = 1
source
theorem Polynomial.scaleRoots_eval₂_mul_of_commute {S : Type u_2} {A : Type u_3} [Semiring S] [Semiring A] {p : Polynomial S} (f : S →+* A) (a : A) (s : S) (hsa : Commute (f s) a) (hf : ∀ (s₁ s₂ : S), Commute (f s₁) (f s₂)) :
eval₂ f (f s * a) (p.scaleRoots s) = f s ^ p.natDegree * eval₂ f a p
source
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) :
eval₂ f (f s * r) (p.scaleRoots s) = f s ^ p.natDegree * eval₂ f r p
source
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 : eval₂ f r p = 0) :
eval₂ f (f s * r) (p.scaleRoots s) = 0
source
theorem Polynomial.scaleRoots_aeval_eq_zero {R : Type u_1} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] {p : Polynomial R} {a : A} {r : R} (ha : (aeval a) p = 0) :
(aeval ((algebraMap R A) r * a)) (p.scaleRoots r) = 0
source
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} (hr : eval₂ f (f r / f s) p = 0) (hs : s ∈ nonZeroDivisors S) :
eval₂ f (f r) (p.scaleRoots s) = 0
source
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 s : R} (hr : (aeval ((algebraMap R K) r / (algebraMap R K) s)) p = 0) (hs : s ∈ nonZeroDivisors R) :
(aeval ((algebraMap R K) r)) (p.scaleRoots s) = 0
source
@[simp]
theorem Polynomial.scaleRoots_mul {R : Type u_1} [CommSemiring R] (p : Polynomial R) (r s : R) :
p.scaleRoots (r * s) = (p.scaleRoots r).scaleRoots s
source
theorem Polynomial.mul_scaleRoots {R : Type u_1} [CommSemiring R] (p q : Polynomial R) (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'`.

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

Alias of `Polynomial.scaleRoots_dvd`.

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

Alias of `Polynomial.scaleRoots_dvd_iff`.

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

Alias of `Polynomial.isCoprime_scaleRoots`.