span_minpoly_eq_annihilator — Mathlib

English

For a linear endomorphism f of a module M over 𝕜, the ideal generated by its minimal polynomial equals the annihilator of f under the evaluation action, i.e. span{minpoly f} = annihilator of f.

Русский

Для линейного отображения f модуля M над 𝕜, идеал, порождаемый минимальным полином, равен аннигилятору f при действии по оценке: span{minpoly f} = annhilator(f).

LaTeX

$$$\operatorname{span}\{\minpoly_{\mathbb{k}}(f)\} = \operatorname{Ann}_{\mathbb{k}[X]}(\mathrm{AEval}'(f)).$$$

Lean4

theorem span_minpoly_eq_annihilator {M} [AddCommGroup M] [Module 𝕜 M] (f : Module.End 𝕜 M) :
    Ideal.span {minpoly 𝕜 f} = Module.annihilator 𝕜[X] (Module.AEval' f) :=
  by
  rw [← annIdealGenerator_eq_minpoly, span_singleton_annIdealGenerator]; ext
  rw [mem_annIdeal_iff_aeval_eq_zero, DFunLike.ext_iff, Module.mem_annihilator]; rfl

Похожие утверждения