annihilator_eq_top_iff — Mathlib

English

The annihilator equals the top ideal if and only if the module is subsingleton.

Русский

Аннигилятор модуля равен верхнему идеалу тогда и только тогда, когда модуль является синглтонным.

LaTeX

$$$\\operatorname{Ann}_R(M) = \\top \\iff \\text{Subsingleton } M$$$

Lean4

theorem annihilator_eq_top_iff : annihilator R M = ⊤ ↔ Subsingleton M :=
  ⟨fun h ↦
    ⟨fun m m' ↦ by
      rw [← one_smul R m, ← one_smul R m']
      simp_rw [mem_annihilator.mp (h ▸ Submodule.mem_top)]⟩,
    fun _ ↦ top_le_iff.mp fun _ _ ↦ mem_annihilator.mpr fun _ ↦ Subsingleton.elim _ _⟩

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