English
If a polynomial p is monic and spans the annihilating ideal annIdeal 𝕜 a, then annIdealGenerator 𝕜 a = p.
Русский
Если полином p монический и генерирует аннигиляторный идеал annIdeal 𝕜 a, то annIdealGenerator 𝕜 a = p.
LaTeX
$$$\text{If } p\text{ is monic and }\operatorname{span}\{p\} = \operatorname{annIdeal}_{\mathbb{k}}(a), \; \operatorname{annIdealGenerator}_{\mathbb{k}}(a) = p.$$$
Lean4
/-- If a monic generates the annihilating ideal, it must match our choice
of the annihilating ideal generator. -/
theorem monic_generator_eq_minpoly (a : A) (p : 𝕜[X]) (p_monic : p.Monic) (p_gen : Ideal.span { p } = annIdeal 𝕜 a) :
annIdealGenerator 𝕜 a = p := by
by_cases h : p = 0
· rwa [h, annIdealGenerator_eq_zero_iff, ← p_gen, Ideal.span_singleton_eq_bot.mpr]
· rw [← span_singleton_annIdealGenerator, Ideal.span_singleton_eq_span_singleton] at p_gen
rw [eq_comm]
apply eq_of_monic_of_associated p_monic _ p_gen
apply monic_annIdealGenerator _ _ ((Associated.ne_zero_iff p_gen).mp h)
