mathlib3 documentation

ring_theory.polynomial.scale_roots

Scaling the roots of a polynomial #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines scale_roots 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.scale_roots {R : Type u_3} [comm_ring R] (p : polynomial R) (s : R) :

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

Equations
@[simp]
theorem polynomial.coeff_scale_roots {R : Type u_3} [comm_ring R] (p : polynomial R) (s : R) (i : ) :
(p.scale_roots s).coeff i = p.coeff i * s ^ (p.nat_degree - i)
@[simp]
theorem polynomial.zero_scale_roots {R : Type u_3} [comm_ring R] (s : R) :
theorem polynomial.scale_roots_ne_zero {R : Type u_3} [comm_ring R] {p : polynomial R} (hp : p 0) (s : R) :
theorem polynomial.support_scale_roots_eq {R : Type u_3} [comm_ring R] (p : polynomial R) {s : R} (hs : s non_zero_divisors R) :
@[simp]
theorem polynomial.degree_scale_roots {R : Type u_3} [comm_ring R] (p : polynomial R) {s : R} :
@[simp]
theorem polynomial.monic_scale_roots_iff {R : Type u_3} [comm_ring R] {p : polynomial R} (s : R) :
theorem polynomial.scale_roots_eval₂_mul {R : Type u_3} {S : Type u_4} [comm_ring R] [comm_ring S] {p : polynomial S} (f : S →+* R) (r : R) (s : S) :
theorem polynomial.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} (hr : polynomial.eval₂ f r p = 0) :
theorem polynomial.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} (hr : (polynomial.aeval r) p = 0) :
theorem polynomial.scale_roots_eval₂_eq_zero_of_eval₂_div_eq_zero {A : Type u_1} {K : Type u_2} [comm_ring A] [is_domain A] [field K] {p : polynomial A} {f : A →+* K} (hf : function.injective f) {r s : A} (hr : polynomial.eval₂ f (f r / f s) p = 0) (hs : s non_zero_divisors A) :
theorem polynomial.map_scale_roots {R : Type u_3} {S : Type u_4} [comm_ring R] [comm_ring S] (p : polynomial R) (x : R) (f : R →+* S) (h : f p.leading_coeff 0) :