case intro.intro
𝕜 : Type u
A : Type v
inst✝⁴ : Field 𝕜
inst✝³ : Ring A
inst✝² : Algebra 𝕜 A
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Nontrivial A
I : FiniteDimensional 𝕜 A
a : A
p : 𝕜[X]
h_mon : Monic p
h_eval_p : eval₂ ↑ₐ a p = 0
⊢ Set.Nonempty (σ a)
𝕜 : Type u
A : Type v
inst✝⁴ : Field 𝕜
inst✝³ : Ring A
inst✝² : Algebra 𝕜 A
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Nontrivial A
I : FiniteDimensional 𝕜 A
a : A
⊢ Set.Nonempty (σ a)
obtain ⟨p, ⟨h_mon, h_eval_p⟩⟩ := isIntegral_of_noetherian (IsNoetherian.iff_fg.2 I) a
case intro.intro
𝕜 : Type u
A : Type v
inst✝⁴ : Field 𝕜
inst✝³ : Ring A
inst✝² : Algebra 𝕜 A
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Nontrivial A
I : FiniteDimensional 𝕜 A
a : A
p : 𝕜[X]
h_mon : Monic p
h_eval_p : eval₂ ↑ₐ a p = 0
nu : ¬IsUnit (↑(aeval a) p)
⊢ Set.Nonempty (σ a)
case intro.intro
𝕜 : Type u
A : Type v
inst✝⁴ : Field 𝕜
inst✝³ : Ring A
inst✝² : Algebra 𝕜 A
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Nontrivial A
I : FiniteDimensional 𝕜 A
a : A
p : 𝕜[X]
h_mon : Monic p
h_eval_p : eval₂ ↑ₐ a p = 0
⊢ Set.Nonempty (σ a)
have nu : ¬IsUnit (aeval a p) := by rw [← aeval_def] at h_eval_p ; rw [h_eval_p]; simp
case intro.intro
𝕜 : Type u
A : Type v
inst✝⁴ : Field 𝕜
inst✝³ : Ring A
inst✝² : Algebra 𝕜 A
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Nontrivial A
I : FiniteDimensional 𝕜 A
a : A
p : 𝕜[X]
h_mon : Monic p
h_eval_p : eval₂ ↑ₐ a p = 0
nu : ¬IsUnit (↑(aeval a) (Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots p))))
⊢ Set.Nonempty (σ a)
case intro.intro
𝕜 : Type u
A : Type v
inst✝⁴ : Field 𝕜
inst✝³ : Ring A
inst✝² : Algebra 𝕜 A
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Nontrivial A
I : FiniteDimensional 𝕜 A
a : A
p : 𝕜[X]
h_mon : Monic p
h_eval_p : eval₂ ↑ₐ a p = 0
nu : ¬IsUnit (↑(aeval a) p)
⊢ Set.Nonempty (σ a)
rw [eq_prod_roots_of_monic_of_splits_id h_mon (IsAlgClosed.splits p)] at nu
case intro.intro.intro.intro
𝕜 : Type u
A : Type v
inst✝⁴ : Field 𝕜
inst✝³ : Ring A
inst✝² : Algebra 𝕜 A
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Nontrivial A
I : FiniteDimensional 𝕜 A
a : A
p : 𝕜[X]
h_mon : Monic p
h_eval_p : eval₂ ↑ₐ a p = 0
nu : ¬IsUnit (↑(aeval a) (Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots p))))
k : 𝕜
hk : k ∈ σ a
right✝ : eval k p = 0
⊢ Set.Nonempty (σ a)
case intro.intro
𝕜 : Type u
A : Type v
inst✝⁴ : Field 𝕜
inst✝³ : Ring A
inst✝² : Algebra 𝕜 A
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Nontrivial A
I : FiniteDimensional 𝕜 A
a : A
p : 𝕜[X]
h_mon : Monic p
h_eval_p : eval₂ ↑ₐ a p = 0
nu : ¬IsUnit (↑(aeval a) (Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots p))))
⊢ Set.Nonempty (σ a)
obtain ⟨k, hk, _⟩ := exists_mem_of_not_isUnit_aeval_prod nu
no goals
case intro.intro.intro.intro
𝕜 : Type u
A : Type v
inst✝⁴ : Field 𝕜
inst✝³ : Ring A
inst✝² : Algebra 𝕜 A
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Nontrivial A
I : FiniteDimensional 𝕜 A
a : A
p : 𝕜[X]
h_mon : Monic p
h_eval_p : eval₂ ↑ₐ a p = 0
nu : ¬IsUnit (↑(aeval a) (Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots p))))
k : 𝕜
hk : k ∈ σ a
right✝ : eval k p = 0
⊢ Set.Nonempty (σ a)
exact ⟨k, hk⟩
𝕜 : Type u
A : Type v
inst✝⁴ : Field 𝕜
inst✝³ : Ring A
inst✝² : Algebra 𝕜 A
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Nontrivial A
I : FiniteDimensional 𝕜 A
a : A
p : 𝕜[X]
h_mon : Monic p
h_eval_p : ↑(aeval a) p = 0
⊢ ¬IsUnit (↑(aeval a) p)
𝕜 : Type u
A : Type v
inst✝⁴ : Field 𝕜
inst✝³ : Ring A
inst✝² : Algebra 𝕜 A
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Nontrivial A
I : FiniteDimensional 𝕜 A
a : A
p : 𝕜[X]
h_mon : Monic p
h_eval_p : eval₂ ↑ₐ a p = 0
⊢ ¬IsUnit (↑(aeval a) p)
rw [← aeval_def] at h_eval_p
𝕜 : Type u
A : Type v
inst✝⁴ : Field 𝕜
inst✝³ : Ring A
inst✝² : Algebra 𝕜 A
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Nontrivial A
I : FiniteDimensional 𝕜 A
a : A
p : 𝕜[X]
h_mon : Monic p
h_eval_p : ↑(aeval a) p = 0
⊢ ¬IsUnit 0
𝕜 : Type u
A : Type v
inst✝⁴ : Field 𝕜
inst✝³ : Ring A
inst✝² : Algebra 𝕜 A
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Nontrivial A
I : FiniteDimensional 𝕜 A
a : A
p : 𝕜[X]
h_mon : Monic p
h_eval_p : ↑(aeval a) p = 0
⊢ ¬IsUnit (↑(aeval a) p)
rw [h_eval_p]
no goals
𝕜 : Type u
A : Type v
inst✝⁴ : Field 𝕜
inst✝³ : Ring A
inst✝² : Algebra 𝕜 A
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Nontrivial A
I : FiniteDimensional 𝕜 A
a : A
p : 𝕜[X]
h_mon : Monic p
h_eval_p : ↑(aeval a) p = 0
⊢ ¬IsUnit 0
simp