mem_annihilator — Mathlib

English

An element r lies in the annihilator of N exactly when r kills every element of N.

Русский

Элемент r принадлежит аннигилятору N тогда и только тогда, когда r убивает каждый элемент N.

LaTeX

$$$ r \\in N.annihilator \\iff \\forall n \\in N,\; r \\cdot n = 0. $$$

Lean4

theorem mem_annihilator {r} : r ∈ N.annihilator ↔ ∀ n ∈ N, r • n = (0 : M) := by
  simp_rw [annihilator, Module.mem_annihilator, Subtype.forall, Subtype.ext_iff]; rfl

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