Documentation

Mathlib.RingTheory.Polynomial.ScaleRoots

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) :

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

Equations
Instances For
    @[simp]
    theorem Polynomial.zero_scaleRoots {R : Type u_1} [Semiring R] (s : R) :
    theorem Polynomial.scaleRoots_ne_zero {R : Type u_1} [Semiring R] {p : Polynomial R} (hp : p 0) (s : R) :
    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) :
    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) :
    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) :
    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) :
    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) :
    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) :