mathlib documentation

ring_theory.polynomial.scale_roots

def scale_roots {R : Type u_3} [comm_ring R] :
polynomial RR → polynomial R

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

Equations
@[simp]
theorem coeff_scale_roots {R : Type u_3} [comm_ring R] (p : polynomial R) (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 : polynomial R) (s : R) :

@[simp]
theorem zero_scale_roots {R : Type u_3} [comm_ring R] (s : R) :

theorem scale_roots_ne_zero {R : Type u_3} [comm_ring R] {p : polynomial R} (hp : p 0) (s : R) :

theorem support_scale_roots_le {R : Type u_3} [comm_ring R] (p : polynomial R) (s : R) :

theorem support_scale_roots_eq {R : Type u_3} [comm_ring R] (p : polynomial R) {s : R} :

@[simp]
theorem degree_scale_roots {R : Type u_3} [comm_ring R] (p : polynomial R) {s : R} :

@[simp]
theorem nat_degree_scale_roots {R : Type u_3} [comm_ring R] (p : polynomial R) (s : R) :

theorem monic_scale_roots_iff {R : Type u_3} [comm_ring R] {p : polynomial R} (s : R) :

theorem scale_roots_eval₂_eq_zero {R : Type u_3} {S : Type u_4} [comm_ring R] [comm_ring S] {p : polynomial S} (f : S →+* R) {r : R} {s : S} :
polynomial.eval₂ f r p = 0polynomial.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 : polynomial S} {r : R} {s : S} :

theorem scale_roots_eval₂_eq_zero_of_eval₂_div_eq_zero {A : Type u_1} {K : Type u_2} [integral_domain A] [field K] {p : polynomial A} {f : A →+* K} (hf : function.injective f) {r s : A} :

theorem scale_roots_aeval_eq_zero_of_aeval_div_eq_zero {A : Type u_1} {K : Type u_2} [integral_domain A] [field K] [algebra A K] (inj : function.injective (algebra_map A K)) {p : polynomial A} {r s : A} :