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 : R
hroot : IsRoot f x
hmo : Monic f
i : ℕ
hi : natDegree f ≤ i
⊢ x ^ i ∈ 𝓟
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 : R
hroot : IsRoot f x
hmo : Monic f
⊢ ∀ (i : ℕ), natDegree f ≤ i → x ^ i ∈ 𝓟
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 : R
hroot : IsRoot f x
hmo : Monic f
i : ℕ
hi : natDegree f ≤ i
k : ℕ
hk : i = natDegree f + k
⊢ x ^ i ∈ 𝓟
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 : R
hroot : IsRoot f x
hmo : Monic f
i : ℕ
hi : natDegree f ≤ i
⊢ x ^ i ∈ 𝓟
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 : R
hroot : IsRoot f x
hmo : Monic f
i : ℕ
hi : natDegree f ≤ i
k : ℕ
hk : i = natDegree f + k
⊢ x ^ natDegree f * x ^ k ∈ 𝓟
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 : R
hroot : IsRoot f x
hmo : Monic f
i : ℕ
hi : natDegree f ≤ i
k : ℕ
hk : i = natDegree f + k
⊢ x ^ i ∈ 𝓟
rw [hk, pow_add]
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 : R
hroot : IsRoot f x
hmo : Monic f
i : ℕ
hi : natDegree f ≤ i
k : ℕ
hk : i = natDegree f + k
⊢ x ^ natDegree f ∈ 𝓟
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 : R
hroot : IsRoot f x
hmo : Monic f
i : ℕ
hi : natDegree f ≤ i
k : ℕ
hk : i = natDegree f + k
⊢ x ^ natDegree f * x ^ k ∈ 𝓟
suffices x ^ f.natDegree ∈ 𝓟 by exact mul_mem_right (x ^ k) 𝓟 this
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 : R
hroot : x ^ natDegree f + ∑ i : Fin (natDegree f), coeff f ↑i * x ^ ↑i = 0
hmo : Monic f
i : ℕ
hi : natDegree f ≤ i
k : ℕ
hk : i = natDegree f + k
⊢ x ^ natDegree f ∈ 𝓟
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 : R
hroot : IsRoot f x
hmo : Monic f
i : ℕ
hi : natDegree f ≤ i
k : ℕ
hk : i = natDegree f + k
⊢ x ^ natDegree f ∈ 𝓟
rw [IsRoot.def, eval_eq_sum_range, Finset.range_add_one,
  Finset.sum_insert Finset.not_mem_range_self, Finset.sum_range, hmo.coeff_natDegree, one_mul] at
  *
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 : R
hroot : x ^ natDegree f + ∑ i : Fin (natDegree f), coeff f ↑i * x ^ ↑i = 0
hmo : Monic f
i : ℕ
hi : natDegree f ≤ i
k : ℕ
hk : i = natDegree f + k
⊢ ∑ i : Fin (natDegree f), coeff f ↑i * x ^ ↑i ∈ 𝓟
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 : R
hroot : x ^ natDegree f + ∑ i : Fin (natDegree f), coeff f ↑i * x ^ ↑i = 0
hmo : Monic f
i : ℕ
hi : natDegree f ≤ i
k : ℕ
hk : i = natDegree f + k
⊢ x ^ natDegree f ∈ 𝓟
rw [eq_neg_of_add_eq_zero_left hroot, Ideal.neg_mem_iff]
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 : R
hroot : x ^ natDegree f + ∑ i : Fin (natDegree f), coeff f ↑i * x ^ ↑i = 0
hmo : Monic f
i : ℕ
hi : natDegree f ≤ i
k : ℕ
hk : i = natDegree f + k
⊢ ∑ i : Fin (natDegree f), coeff f ↑i * x ^ ↑i ∈ 𝓟
refine' Submodule.sum_mem _ fun i _ => mul_mem_right _ _ (hf.mem (Fin.is_lt i))
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 : R
hroot : IsRoot f x
hmo : Monic f
i : ℕ
hi : natDegree f ≤ i
k : ℕ
hk : i = natDegree f + k
this : x ^ natDegree f ∈ 𝓟
⊢ x ^ natDegree f * x ^ k ∈ 𝓟
exact mul_mem_right (x ^ k) 𝓟 this