English
The generator of the annihilating ideal is the minimal polynomial of the element, i.e. annIdealGenerator 𝕜 a = minpoly 𝕜 a (including the zero case where both sides are zero).
Русский
Генератор аннигиляторного идеала совпадает с минимальным полиномом элемента: annIdealGenerator 𝕜 a = minpoly 𝕜 a (включая нулевой случай).
LaTeX
$$$\operatorname{annIdealGenerator}_{\mathbb{k}}(a) = \operatorname{minpoly}_{\mathbb{k}}(a).$$$
Lean4
/-- The generator of the annihilating ideal is the minimal polynomial. -/
theorem annIdealGenerator_eq_minpoly (a : A) : annIdealGenerator 𝕜 a = minpoly 𝕜 a :=
by
by_cases h : annIdealGenerator 𝕜 a = 0
· rw [h, minpoly.eq_zero]
rintro ⟨p, p_monic, hp : aeval a p = 0⟩
refine p_monic.ne_zero (Ideal.mem_bot.mp ?_)
simpa only [annIdealGenerator_eq_zero_iff.mp h] using mem_annIdeal_iff_aeval_eq_zero.mpr hp
·
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
