mem_annihilator_span_singleton — Mathlib

English

For a single generator g, r belongs to the annihilator of its span iff r·g = 0.

Русский

Для фиксированного порождающего элемента g: r принадлежит аннигилятору охвата {g} тогда и только тогда, когда r·g = 0.

LaTeX

$$$ r \\in (\\operatorname{span}_R(\\{g\\}))\\.annihilator \\iff r \\cdot g = 0. $$$

Lean4

theorem mem_annihilator_span_singleton (g : M) (r : R) :
    r ∈ (Submodule.span R ({ g } : Set M)).annihilator ↔ r • g = 0 := by simp [mem_annihilator_span]

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