English
The span of the singleton annIdealGenerator 𝕜 a generates the annihilating ideal: span{annIdealGenerator 𝕜 a} = annIdeal 𝕜 a.
Русский
Общий порожденный идеал аннигиляционной аннигиляции: span{annIdealGenerator 𝕜 a} = annIdeal 𝕜 a.
LaTeX
$$$\operatorname{span}\{\operatorname{annIdealGenerator}_{\mathbb{k}}(a)\} = \operatorname{annIdeal}_{\mathbb{k}}(a).$$$
Lean4
/-- `annIdealGenerator 𝕜 a` is indeed a generator. -/
@[simp]
theorem span_singleton_annIdealGenerator (a : A) : Ideal.span {annIdealGenerator 𝕜 a} = annIdeal 𝕜 a :=
by
by_cases h : annIdealGenerator 𝕜 a = 0
· rw [h, annIdealGenerator_eq_zero_iff.mp h, Set.singleton_zero, Ideal.span_zero]
· rw [annIdealGenerator, Ideal.span_singleton_mul_right_unit, Ideal.span_singleton_generator]
apply Polynomial.isUnit_C.mpr
apply IsUnit.mk0
apply inv_eq_zero.not.mpr
apply Polynomial.leadingCoeff_eq_zero.not.mpr
apply (mul_ne_zero_iff.mp h).1
