R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf✝ : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hx : ↑(aeval x) f = 0
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
i : ℕ
hi : natDegree (Polynomial.map (algebraMap R S) f) ≤ i
⊢ ∃ y, y ∈ adjoin R {x} ∧ ↑(algebraMap R S) p * y = 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
p : R
x : S
hx : ↑(aeval x) f = 0
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
⊢ ∀ (i : ℕ), natDegree (Polynomial.map (algebraMap R S) f) ≤ i → ∃ y, y ∈ adjoin R {x} ∧ ↑(algebraMap R S) p * y = 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
p : R
x : S
hx : ↑(aeval x) f = 0
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
i : ℕ
hi : natDegree (Polynomial.map (algebraMap R S) f) ≤ i
k : ℕ
hk : i = natDegree (Polynomial.map (algebraMap R S) f) + k
⊢ ∃ y, y ∈ adjoin R {x} ∧ ↑(algebraMap R S) p * y = 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
p : R
x : S
hx : ↑(aeval x) f = 0
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
i : ℕ
hi : natDegree (Polynomial.map (algebraMap R S) f) ≤ i
⊢ ∃ y, y ∈ adjoin R {x} ∧ ↑(algebraMap R S) p * y = 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
p : R
x : S
hx : ↑(aeval x) f = 0
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
i : ℕ
hi : natDegree (Polynomial.map (algebraMap R S) f) ≤ i
k : ℕ
hk : i = natDegree (Polynomial.map (algebraMap R S) f) + k
⊢ ∃ y, y ∈ adjoin R {x} ∧ ↑(algebraMap R S) p * y = x ^ natDegree (Polynomial.map (algebraMap R S) 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
p : R
x : S
hx : ↑(aeval x) f = 0
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
i : ℕ
hi : natDegree (Polynomial.map (algebraMap R S) f) ≤ i
k : ℕ
hk : i = natDegree (Polynomial.map (algebraMap R S) f) + k
⊢ ∃ y, y ∈ adjoin R {x} ∧ ↑(algebraMap R S) p * y = x ^ i
rw [hk, pow_add]
case intro.intro.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
p : R
x : S
hx : ↑(aeval x) f = 0
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
i : ℕ
hi : natDegree (Polynomial.map (algebraMap R S) f) ≤ i
k : ℕ
hk : i = natDegree (Polynomial.map (algebraMap R S) f) + k
y : S
hy : y ∈ adjoin R {x}
H : ↑(algebraMap R S) p * y = x ^ natDegree (Polynomial.map (algebraMap R S) f)
⊢ ∃ y, y ∈ adjoin R {x} ∧ ↑(algebraMap R S) p * y = x ^ natDegree (Polynomial.map (algebraMap R S) 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
p : R
x : S
hx : ↑(aeval x) f = 0
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
i : ℕ
hi : natDegree (Polynomial.map (algebraMap R S) f) ≤ i
k : ℕ
hk : i = natDegree (Polynomial.map (algebraMap R S) f) + k
⊢ ∃ y, y ∈ adjoin R {x} ∧ ↑(algebraMap R S) p * y = x ^ natDegree (Polynomial.map (algebraMap R S) f) * x ^ k
obtain ⟨y, hy, H⟩ := exists_mem_adjoin_mul_eq_pow_natDegree hx hmo hf
case intro.intro.intro.refine'_1
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf✝ : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hx : ↑(aeval x) f = 0
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
i : ℕ
hi : natDegree (Polynomial.map (algebraMap R S) f) ≤ i
k : ℕ
hk : i = natDegree (Polynomial.map (algebraMap R S) f) + k
y : S
hy : y ∈ adjoin R {x}
H : ↑(algebraMap R S) p * y = x ^ natDegree (Polynomial.map (algebraMap R S) f)
⊢ y * x ^ k ∈ adjoin R {x}

case intro.intro.intro.refine'_2
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf✝ : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hx : ↑(aeval x) f = 0
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
i : ℕ
hi : natDegree (Polynomial.map (algebraMap R S) f) ≤ i
k : ℕ
hk : i = natDegree (Polynomial.map (algebraMap R S) f) + k
y : S
hy : y ∈ adjoin R {x}
H : ↑(algebraMap R S) p * y = x ^ natDegree (Polynomial.map (algebraMap R S) f)
⊢ ↑(algebraMap R S) p * (y * x ^ k) = x ^ natDegree (Polynomial.map (algebraMap R S) f) * x ^ k
case intro.intro.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
p : R
x : S
hx : ↑(aeval x) f = 0
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
i : ℕ
hi : natDegree (Polynomial.map (algebraMap R S) f) ≤ i
k : ℕ
hk : i = natDegree (Polynomial.map (algebraMap R S) f) + k
y : S
hy : y ∈ adjoin R {x}
H : ↑(algebraMap R S) p * y = x ^ natDegree (Polynomial.map (algebraMap R S) f)
⊢ ∃ y, y ∈ adjoin R {x} ∧ ↑(algebraMap R S) p * y = x ^ natDegree (Polynomial.map (algebraMap R S) f) * x ^ k
refine' ⟨y * x ^ k, _, _⟩
no goals
case intro.intro.intro.refine'_1
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf✝ : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hx : ↑(aeval x) f = 0
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
i : ℕ
hi : natDegree (Polynomial.map (algebraMap R S) f) ≤ i
k : ℕ
hk : i = natDegree (Polynomial.map (algebraMap R S) f) + k
y : S
hy : y ∈ adjoin R {x}
H : ↑(algebraMap R S) p * y = x ^ natDegree (Polynomial.map (algebraMap R S) f)
⊢ y * x ^ k ∈ adjoin R {x}
exact Subalgebra.mul_mem _ hy (Subalgebra.pow_mem _ (subset_adjoin (Set.mem_singleton x)) _)
no goals
case intro.intro.intro.refine'_2
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf✝ : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hx : ↑(aeval x) f = 0
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
i : ℕ
hi : natDegree (Polynomial.map (algebraMap R S) f) ≤ i
k : ℕ
hk : i = natDegree (Polynomial.map (algebraMap R S) f) + k
y : S
hy : y ∈ adjoin R {x}
H : ↑(algebraMap R S) p * y = x ^ natDegree (Polynomial.map (algebraMap R S) f)
⊢ ↑(algebraMap R S) p * (y * x ^ k) = x ^ natDegree (Polynomial.map (algebraMap R S) f) * x ^ k
rw [← mul_assoc _ y, H]