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:
```lean
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
```




Co-authored-by: Johan Commelin <[email protected]>

Mathlib/Data/Polynomial/Module.lean

@@ -88,6 +88,14 @@ instance instIsScalarTowerOrigPolynomial : IsScalarTower R R[X] <| AEval R M a w
 instance instFinitePolynomial [Finite R M] : Finite R[X] <| AEval R M a :=
   Finite.of_restrictScalars_finite R _ _
 
+@[simp]
+lemma annihilator_top_eq_ker_aeval [FaithfulSMul A M] :
+    (⊤ : Submodule R[X] <| AEval R M a).annihilator = RingHom.ker (aeval a) := by
+  ext p
+  simp only [Submodule.mem_annihilator, Submodule.mem_top, forall_true_left, RingHom.mem_ker]
+  change (∀ m : M, aeval a p • m = 0) ↔ _
+  exact ⟨fun h ↦ eq_of_smul_eq_smul (α := M) <| by simp [h], fun h ↦ by simp [h]⟩
+
 section Submodule
 
 variable {p : Submodule R M} (hp : p ≤ p.comap (Algebra.lsmul R R M a))

Mathlib/FieldTheory/Minpoly/Field.lean

@@ -78,6 +78,10 @@ theorem dvd {p : A[X]} (hp : Polynomial.aeval x p = 0) : minpoly A x ∣ p := by
   exact degree_modByMonic_lt _ (monic hx)
 #align minpoly.dvd minpoly.dvd
 
+variable {A x} in
+lemma dvd_iff {p : A[X]} : minpoly A x ∣ p ↔ Polynomial.aeval x p = 0 :=
+  ⟨fun ⟨q, hq⟩ ↦ by rw [hq, map_mul, aeval, zero_mul], minpoly.dvd A x⟩
+
 theorem dvd_map_of_isScalarTower (A K : Type*) {R : Type*} [CommRing A] [Field K] [CommRing R]
     [Algebra A K] [Algebra A R] [Algebra K R] [IsScalarTower A K R] (x : R) :
     minpoly K x ∣ (minpoly A x).map (algebraMap A K) := by
@@ -104,6 +108,15 @@ theorem aeval_of_isScalarTower (R : Type*) {K T U : Type*} [CommRing R] [Field K
       (minpoly.dvd_map_of_isScalarTower R K x) hy
 #align minpoly.aeval_of_is_scalar_tower minpoly.aeval_of_isScalarTower
 
+/-- See also `minpoly.ker_eval` which relaxes the assumptions on `A` in exchange for
+stronger assumptions on `B`. -/
+@[simp]
+lemma ker_aeval_eq_span_minpoly :
+    RingHom.ker (Polynomial.aeval x) = A[X] ∙ minpoly A x := by
+  ext p
+  simp_rw [RingHom.mem_ker, ← minpoly.dvd_iff, Submodule.mem_span_singleton,
+    dvd_iff_exists_eq_mul_left, smul_eq_mul, eq_comm (a := p)]
+
 variable {A x}
 
 theorem eq_of_irreducible_of_monic [Nontrivial B] {p : A[X]} (hp1 : Irreducible p)