R : Type u
inst✝¹ : CommSemiring R
𝓟 : Ideal R
f : R[X]
hf : IsWeaklyEisensteinAt f 𝓟
A : Type v
inst✝ : CommRing A
φ : R →+* A
n✝ : ℕ
hn : n✝ < natDegree (Polynomial.map φ f)
⊢ coeff (Polynomial.map φ f) n✝ ∈ Ideal.map φ 𝓟
R : Type u
inst✝¹ : CommSemiring R
𝓟 : Ideal R
f : R[X]
hf : IsWeaklyEisensteinAt f 𝓟
A : Type v
inst✝ : CommRing A
φ : R →+* A
⊢ IsWeaklyEisensteinAt (Polynomial.map φ f) (Ideal.map φ 𝓟)
refine' (IsWeaklyEisensteinAt_iff _ _).2 fun hn => _
R : Type u
inst✝¹ : CommSemiring R
𝓟 : Ideal R
f : R[X]
hf : IsWeaklyEisensteinAt f 𝓟
A : Type v
inst✝ : CommRing A
φ : R →+* A
n✝ : ℕ
hn : n✝ < natDegree (Polynomial.map φ f)
⊢ ↑φ (coeff f n✝) ∈ Ideal.map φ 𝓟
R : Type u
inst✝¹ : CommSemiring R
𝓟 : Ideal R
f : R[X]
hf : IsWeaklyEisensteinAt f 𝓟
A : Type v
inst✝ : CommRing A
φ : R →+* A
n✝ : ℕ
hn : n✝ < natDegree (Polynomial.map φ f)
⊢ coeff (Polynomial.map φ f) n✝ ∈ Ideal.map φ 𝓟
rw [coeff_map]
no goals
R : Type u
inst✝¹ : CommSemiring R
𝓟 : Ideal R
f : R[X]
hf : IsWeaklyEisensteinAt f 𝓟
A : Type v
inst✝ : CommRing A
φ : R →+* A
n✝ : ℕ
hn : n✝ < natDegree (Polynomial.map φ f)
⊢ ↑φ (coeff f n✝) ∈ Ideal.map φ 𝓟
exact mem_map_of_mem _ (hf.mem (lt_of_lt_of_le hn (natDegree_map_le _ _)))