R : Type u
A : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing A
f : R →+* A
hf : Function.Injective ↑f
p : R[X]
hp : Monic p
x y : R
z : A
h : eval₂ f z p = 0
hz : ↑f x * z = ↑f y
⊢ y ^ natDegree (scaleRoots p x) ∈ span {x}
R : Type u
A : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing A
f : R →+* A
hf : Function.Injective ↑f
p : R[X]
hp : Monic p
x y : R
z : A
h : eval₂ f z p = 0
hz : ↑f x * z = ↑f y
⊢ x ∣ y ^ natDegree p
rw [← natDegree_scaleRoots p x, ← Ideal.mem_span_singleton]
R : Type u
A : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing A
f : R →+* A
hf : Function.Injective ↑f
p : R[X]
hp : Monic p
x y : R
z : A
h : eval₂ f z p = 0
hz : ↑f x * z = ↑f y
⊢ IsRoot (scaleRoots p x) y
R : Type u
A : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing A
f : R →+* A
hf : Function.Injective ↑f
p : R[X]
hp : Monic p
x y : R
z : A
h : eval₂ f z p = 0
hz : ↑f x * z = ↑f y
⊢ y ^ natDegree (scaleRoots p x) ∈ span {x}
refine'
  (scaleRoots.isWeaklyEisensteinAt _
        (Ideal.mem_span_singleton.mpr <| dvd_refl x)).pow_natDegree_le_of_root_of_monic_mem
    _ ((monic_scaleRoots_iff x).mpr hp) _ le_rfl
R : Type u
A : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing A
f : R →+* A
hf : ∀ (a : R), ↑f a = 0 ↔ a = 0
p : R[X]
hp : Monic p
x y : R
z : A
h : eval₂ f z p = 0
hz : ↑f x * z = ↑f y
⊢ IsRoot (scaleRoots p x) y
R : Type u
A : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing A
f : R →+* A
hf : Function.Injective ↑f
p : R[X]
hp : Monic p
x y : R
z : A
h : eval₂ f z p = 0
hz : ↑f x * z = ↑f y
⊢ IsRoot (scaleRoots p x) y
rw [injective_iff_map_eq_zero'] at hf
R : Type u
A : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing A
f : R →+* A
hf : ∀ (a : R), ↑f a = 0 ↔ a = 0
p : R[X]
hp : Monic p
x y : R
z : A
h : eval₂ f z p = 0
hz : ↑f x * z = ↑f y
this : eval₂ f (↑f x * z) (scaleRoots p x) = 0
⊢ IsRoot (scaleRoots p x) y
R : Type u
A : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing A
f : R →+* A
hf : ∀ (a : R), ↑f a = 0 ↔ a = 0
p : R[X]
hp : Monic p
x y : R
z : A
h : eval₂ f z p = 0
hz : ↑f x * z = ↑f y
⊢ IsRoot (scaleRoots p x) y
have : eval₂ _ _ (p.scaleRoots x) = 0 := scaleRoots_eval₂_eq_zero f h
no goals
R : Type u
A : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing A
f : R →+* A
hf : ∀ (a : R), ↑f a = 0 ↔ a = 0
p : R[X]
hp : Monic p
x y : R
z : A
h : eval₂ f z p = 0
hz : ↑f x * z = ↑f y
this : eval₂ f (↑f x * z) (scaleRoots p x) = 0
⊢ IsRoot (scaleRoots p x) y
rwa [hz, Polynomial.eval₂_at_apply, hf] at this