[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
⊢ annIdealGenerator 𝕜 a = 0 ↔ annIdeal 𝕜 a = ⊥
[PROOFSTEP]
simp only [annIdealGenerator, mul_eq_zero, IsPrincipal.eq_bot_iff_generator_eq_zero, Polynomial.C_eq_zero, inv_eq_zero,
  Polynomial.leadingCoeff_eq_zero, or_self_iff]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
⊢ Ideal.span {annIdealGenerator 𝕜 a} = annIdeal 𝕜 a
[PROOFSTEP]
by_cases h : annIdealGenerator 𝕜 a = 0
[GOAL]
case pos
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
h : annIdealGenerator 𝕜 a = 0
⊢ Ideal.span {annIdealGenerator 𝕜 a} = annIdeal 𝕜 a
[PROOFSTEP]
rw [h, annIdealGenerator_eq_zero_iff.mp h, Set.singleton_zero, Ideal.span_zero]
[GOAL]
case neg
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
h : ¬annIdealGenerator 𝕜 a = 0
⊢ Ideal.span {annIdealGenerator 𝕜 a} = annIdeal 𝕜 a
[PROOFSTEP]
rw [annIdealGenerator, Ideal.span_singleton_mul_right_unit, Ideal.span_singleton_generator]
[GOAL]
case neg.h2
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
h : ¬annIdealGenerator 𝕜 a = 0
⊢ IsUnit (↑C (leadingCoeff (IsPrincipal.generator (annIdeal 𝕜 a)))⁻¹)
[PROOFSTEP]
apply Polynomial.isUnit_C.mpr
[GOAL]
case neg.h2
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
h : ¬annIdealGenerator 𝕜 a = 0
⊢ IsUnit (leadingCoeff (IsPrincipal.generator (annIdeal 𝕜 a)))⁻¹
[PROOFSTEP]
apply IsUnit.mk0
[GOAL]
case neg.h2.hx
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
h : ¬annIdealGenerator 𝕜 a = 0
⊢ (leadingCoeff (IsPrincipal.generator (annIdeal 𝕜 a)))⁻¹ ≠ 0
[PROOFSTEP]
apply inv_eq_zero.not.mpr
[GOAL]
case neg.h2.hx
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
h : ¬annIdealGenerator 𝕜 a = 0
⊢ ¬leadingCoeff (IsPrincipal.generator (annIdeal 𝕜 a)) = 0
[PROOFSTEP]
apply Polynomial.leadingCoeff_eq_zero.not.mpr
[GOAL]
case neg.h2.hx
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
h : ¬annIdealGenerator 𝕜 a = 0
⊢ ¬IsPrincipal.generator (annIdeal 𝕜 a) = 0
[PROOFSTEP]
apply (mul_ne_zero_iff.mp h).1
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
p : 𝕜[X]
a : A
⊢ p ∈ annIdeal 𝕜 a ↔ ∃ s, p = s • annIdealGenerator 𝕜 a
[PROOFSTEP]
simp_rw [@eq_comm _ p, ← mem_span_singleton, ← span_singleton_annIdealGenerator 𝕜 a, Ideal.span]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
p : 𝕜[X]
a : A
⊢ p ∈ annIdeal 𝕜 a ↔ annIdealGenerator 𝕜 a ∣ p
[PROOFSTEP]
rw [← Ideal.mem_span_singleton, span_singleton_annIdealGenerator]
[GOAL]
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
⊢ annIdealGenerator 𝕜 a = minpoly 𝕜 a
[PROOFSTEP]
by_cases h : annIdealGenerator 𝕜 a = 0
[GOAL]
case pos
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
h : annIdealGenerator 𝕜 a = 0
⊢ annIdealGenerator 𝕜 a = minpoly 𝕜 a
[PROOFSTEP]
rw [h, minpoly.eq_zero]
[GOAL]
case pos
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
h : annIdealGenerator 𝕜 a = 0
⊢ ¬IsIntegral 𝕜 a
[PROOFSTEP]
rintro ⟨p, p_monic, hp : aeval a p = 0⟩
[GOAL]
case pos.intro.intro
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
h : annIdealGenerator 𝕜 a = 0
p : 𝕜[X]
p_monic : Monic p
hp : ↑(aeval a) p = 0
⊢ False
[PROOFSTEP]
refine' p_monic.ne_zero (Ideal.mem_bot.mp _)
[GOAL]
case pos.intro.intro
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
h : annIdealGenerator 𝕜 a = 0
p : 𝕜[X]
p_monic : Monic p
hp : ↑(aeval a) p = 0
⊢ p ∈ ⊥
[PROOFSTEP]
simpa only [annIdealGenerator_eq_zero_iff.mp h] using mem_annIdeal_iff_aeval_eq_zero.mpr hp
[GOAL]
case neg
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
h : ¬annIdealGenerator 𝕜 a = 0
⊢ annIdealGenerator 𝕜 a = minpoly 𝕜 a
[PROOFSTEP]
exact
  minpoly.unique _ _ (monic_annIdealGenerator _ _ h) (annIdealGenerator_aeval_eq_zero _ _) fun q q_monic hq =>
    degree_annIdealGenerator_le_of_mem a q (mem_annIdeal_iff_aeval_eq_zero.mpr hq) q_monic.ne_zero
[GOAL]
𝕜 : 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
[PROOFSTEP]
by_cases h : p = 0
[GOAL]
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
[PROOFSTEP]
rwa [h, annIdealGenerator_eq_zero_iff, ← p_gen, Ideal.span_singleton_eq_bot.mpr]
[GOAL]
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
[PROOFSTEP]
rw [← span_singleton_annIdealGenerator, Ideal.span_singleton_eq_span_singleton] at p_gen 
[GOAL]
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
[PROOFSTEP]
rw [eq_comm]
[GOAL]
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
[PROOFSTEP]
apply eq_of_monic_of_associated p_monic _ p_gen
[GOAL]
𝕜 : 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)
[PROOFSTEP]
apply monic_annIdealGenerator _ _ ((Associated.ne_zero_iff p_gen).mp h)
