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

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
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a : A
⊢ Ideal.span {annIdealGenerator 𝕜 a} = annIdeal 𝕜 a
by_cases h : annIdealGenerator 𝕜 a = 0
no goals
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
rw [h, annIdealGenerator_eq_zero_iff.mp h, Set.singleton_zero, Ideal.span_zero]
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)))⁻¹)
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
rw [annIdealGenerator, Ideal.span_singleton_mul_right_unit, Ideal.span_singleton_generator]
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)))⁻¹
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)))⁻¹)
apply Polynomial.isUnit_C.mpr
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
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)))⁻¹
apply IsUnit.mk0
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
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
apply inv_eq_zero.not.mpr
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
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
apply Polynomial.leadingCoeff_eq_zero.not.mpr
no goals
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
apply (mul_ne_zero_iff.mp h).1