annihilator_top_eq_ker_aeval — Mathlib

English

The top submodule's annihilator equals ker(aeval a).

Русский

Аннигилирующий верхний подмодуль равен ker(aeval a).

LaTeX

$$$(\top : Submodule R[X](\ AEval R M a)).annihilator = \ker(\mathrm{aeval}\ a)$$$

Lean4

@[simp]
theorem 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]⟩

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