R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : ↑(aeval x) f = 0
hmo : Monic f
⊢ x ^ natDegree (Polynomial.map (algebraMap R S) f) ∈ Ideal.map (algebraMap R S) 𝓟
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : ↑(aeval x) f = 0
hmo : Monic f
⊢ ∀ (i : ℕ), natDegree (Polynomial.map (algebraMap R S) f) ≤ i → x ^ i ∈ Ideal.map (algebraMap R S) 𝓟
suffices x ^ (f.map (algebraMap R S)).natDegree ∈ 𝓟.map (algebraMap R S) by
  intro i hi
  obtain ⟨k, hk⟩ := exists_add_of_le hi
  rw [hk, pow_add]
  refine' mul_mem_right _ _ this
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsRoot (Polynomial.map (algebraMap R S) f) x
hmo : Monic f
⊢ x ^ natDegree (Polynomial.map (algebraMap R S) f) ∈ Ideal.map (algebraMap R S) 𝓟
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : ↑(aeval x) f = 0
hmo : Monic f
⊢ x ^ natDegree (Polynomial.map (algebraMap R S) f) ∈ Ideal.map (algebraMap R S) 𝓟
rw [aeval_def, eval₂_eq_eval_map, ← IsRoot.def] at hx
no goals
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsRoot (Polynomial.map (algebraMap R S) f) x
hmo : Monic f
⊢ x ^ natDegree (Polynomial.map (algebraMap R S) f) ∈ Ideal.map (algebraMap R S) 𝓟
refine' pow_natDegree_le_of_root_of_monic_mem (hf.map _) hx (hmo.map _) _ rfl.le
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : ↑(aeval x) f = 0
hmo : Monic f
this : x ^ natDegree (Polynomial.map (algebraMap R S) f) ∈ Ideal.map (algebraMap R S) 𝓟
i : ℕ
hi : natDegree (Polynomial.map (algebraMap R S) f) ≤ i
⊢ x ^ i ∈ Ideal.map (algebraMap R S) 𝓟
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : ↑(aeval x) f = 0
hmo : Monic f
this : x ^ natDegree (Polynomial.map (algebraMap R S) f) ∈ Ideal.map (algebraMap R S) 𝓟
⊢ ∀ (i : ℕ), natDegree (Polynomial.map (algebraMap R S) f) ≤ i → x ^ i ∈ Ideal.map (algebraMap R S) 𝓟
intro i hi
case intro
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : ↑(aeval x) f = 0
hmo : Monic f
this : x ^ natDegree (Polynomial.map (algebraMap R S) f) ∈ Ideal.map (algebraMap R S) 𝓟
i : ℕ
hi : natDegree (Polynomial.map (algebraMap R S) f) ≤ i
k : ℕ
hk : i = natDegree (Polynomial.map (algebraMap R S) f) + k
⊢ x ^ i ∈ Ideal.map (algebraMap R S) 𝓟
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : ↑(aeval x) f = 0
hmo : Monic f
this : x ^ natDegree (Polynomial.map (algebraMap R S) f) ∈ Ideal.map (algebraMap R S) 𝓟
i : ℕ
hi : natDegree (Polynomial.map (algebraMap R S) f) ≤ i
⊢ x ^ i ∈ Ideal.map (algebraMap R S) 𝓟
obtain ⟨k, hk⟩ := exists_add_of_le hi
case intro
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : ↑(aeval x) f = 0
hmo : Monic f
this : x ^ natDegree (Polynomial.map (algebraMap R S) f) ∈ Ideal.map (algebraMap R S) 𝓟
i : ℕ
hi : natDegree (Polynomial.map (algebraMap R S) f) ≤ i
k : ℕ
hk : i = natDegree (Polynomial.map (algebraMap R S) f) + k
⊢ x ^ natDegree (Polynomial.map (algebraMap R S) f) * x ^ k ∈ Ideal.map (algebraMap R S) 𝓟
case intro
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : ↑(aeval x) f = 0
hmo : Monic f
this : x ^ natDegree (Polynomial.map (algebraMap R S) f) ∈ Ideal.map (algebraMap R S) 𝓟
i : ℕ
hi : natDegree (Polynomial.map (algebraMap R S) f) ≤ i
k : ℕ
hk : i = natDegree (Polynomial.map (algebraMap R S) f) + k
⊢ x ^ i ∈ Ideal.map (algebraMap R S) 𝓟
rw [hk, pow_add]
no goals
case intro
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : ↑(aeval x) f = 0
hmo : Monic f
this : x ^ natDegree (Polynomial.map (algebraMap R S) f) ∈ Ideal.map (algebraMap R S) 𝓟
i : ℕ
hi : natDegree (Polynomial.map (algebraMap R S) f) ≤ i
k : ℕ
hk : i = natDegree (Polynomial.map (algebraMap R S) f) + k
⊢ x ^ natDegree (Polynomial.map (algebraMap R S) f) * x ^ k ∈ Ideal.map (algebraMap R S) 𝓟
refine' mul_mem_right _ _ this