case pos
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
p_monic : Monic p
p_gen : Ideal.span {p} = annIdeal 𝕜 a
h : p = 0
⊢ annIdealGenerator 𝕜 a = p

case neg
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
p_monic : Monic p
p_gen : Ideal.span {p} = annIdeal 𝕜 a
h : ¬p = 0
⊢ annIdealGenerator 𝕜 a = p
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
p_monic : Monic p
p_gen : Ideal.span {p} = annIdeal 𝕜 a
⊢ annIdealGenerator 𝕜 a = p
by_cases h : p = 0
no goals
case pos
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
p_monic : Monic p
p_gen : Ideal.span {p} = annIdeal 𝕜 a
h : p = 0
⊢ annIdealGenerator 𝕜 a = p
rwa [h, annIdealGenerator_eq_zero_iff, ← p_gen, Ideal.span_singleton_eq_bot.mpr]
case neg
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
p_monic : Monic p
p_gen : Associated p (annIdealGenerator 𝕜 a)
h : ¬p = 0
⊢ annIdealGenerator 𝕜 a = p
case neg
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
p_monic : Monic p
p_gen : Ideal.span {p} = annIdeal 𝕜 a
h : ¬p = 0
⊢ annIdealGenerator 𝕜 a = p
rw [← span_singleton_annIdealGenerator, Ideal.span_singleton_eq_span_singleton] at p_gen
case neg
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
p_monic : Monic p
p_gen : Associated p (annIdealGenerator 𝕜 a)
h : ¬p = 0
⊢ p = annIdealGenerator 𝕜 a
case neg
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
p_monic : Monic p
p_gen : Associated p (annIdealGenerator 𝕜 a)
h : ¬p = 0
⊢ annIdealGenerator 𝕜 a = p
rw [eq_comm]
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
p_monic : Monic p
p_gen : Associated p (annIdealGenerator 𝕜 a)
h : ¬p = 0
⊢ Monic (annIdealGenerator 𝕜 a)
case neg
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
p_monic : Monic p
p_gen : Associated p (annIdealGenerator 𝕜 a)
h : ¬p = 0
⊢ p = annIdealGenerator 𝕜 a
apply eq_of_monic_of_associated p_monic _ p_gen
no goals
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
p : 𝕜[X]
p_monic : Monic p
p_gen : Associated p (annIdealGenerator 𝕜 a)
h : ¬p = 0
⊢ Monic (annIdealGenerator 𝕜 a)
apply monic_annIdealGenerator _ _ ((Associated.ne_zero_iff p_gen).mp h)