R : Type u
A : Type ?u.108344
inst✝¹ : CommRing R
inst✝ : CommRing A
p : R[X]
x : R
P : Ideal R
hP : x ∈ P
n✝ : ℕ
i : n✝ < natDegree (scaleRoots p x)
⊢ coeff (scaleRoots p x) n✝ ∈ P
R : Type u
A : Type ?u.108344
inst✝¹ : CommRing R
inst✝ : CommRing A
p : R[X]
x : R
P : Ideal R
hP : x ∈ P
⊢ IsWeaklyEisensteinAt (scaleRoots p x) P
refine' ⟨fun i => _⟩
R : Type u
A : Type ?u.108344
inst✝¹ : CommRing R
inst✝ : CommRing A
p : R[X]
x : R
P : Ideal R
hP : x ∈ P
n✝ : ℕ
i : n✝ < natDegree (scaleRoots p x)
⊢ coeff p n✝ * x ^ (natDegree p - n✝) ∈ P
R : Type u
A : Type ?u.108344
inst✝¹ : CommRing R
inst✝ : CommRing A
p : R[X]
x : R
P : Ideal R
hP : x ∈ P
n✝ : ℕ
i : n✝ < natDegree (scaleRoots p x)
⊢ coeff (scaleRoots p x) n✝ ∈ P
rw [coeff_scaleRoots]
R : Type u
A : Type ?u.108344
inst✝¹ : CommRing R
inst✝ : CommRing A
p : R[X]
x : R
P : Ideal R
hP : x ∈ P
n✝ : ℕ
i✝ : n✝ < natDegree p
i : 0 < natDegree p - n✝
⊢ coeff p n✝ * x ^ (natDegree p - n✝) ∈ P
R : Type u
A : Type ?u.108344
inst✝¹ : CommRing R
inst✝ : CommRing A
p : R[X]
x : R
P : Ideal R
hP : x ∈ P
n✝ : ℕ
i : n✝ < natDegree (scaleRoots p x)
⊢ coeff p n✝ * x ^ (natDegree p - n✝) ∈ P
rw [natDegree_scaleRoots, ← tsub_pos_iff_lt] at i
no goals
R : Type u
A : Type ?u.108344
inst✝¹ : CommRing R
inst✝ : CommRing A
p : R[X]
x : R
P : Ideal R
hP : x ∈ P
n✝ : ℕ
i✝ : n✝ < natDegree p
i : 0 < natDegree p - n✝
⊢ coeff p n✝ * x ^ (natDegree p - n✝) ∈ P
exact Ideal.mul_mem_left _ _ (Ideal.pow_mem_of_mem P hP _ i)