Commit 2024-01-26 04:28 970a1ab2

feat: the minimal polynomial is a generator of the annihilator ideal (#10008) More precisely, the goal of these changes is to make the following work:

import Mathlib.FieldTheory.Minpoly.Field
open Module Polynomial
example {K V : Type*} [Field K] [AddCommGroup V] [Module K V] (f : End K V) :
    (⊤ : Submodule K[X] <| AEval K V f).annihilator = K[X] ∙ minpoly K f := by
  simp