mem_colon_singleton — Mathlib

English

Let N ⊆ M be a submodule and x ∈ M. Then r ∈ N.colon (span{ x }) if and only if r • x ∈ N.

Русский

Пусть N — подмодуль M и x ∈ M. Тогда r ∈ N.colon(span{x}) тогда и только тогда, когда r·x ∈ N.

LaTeX

$$$ r \\in N : \\mathrm{span}\\,\\{ x \\} \\iff r \\cdot x \\in N $$$

Lean4

@[simp]
theorem mem_colon_singleton {x : M} {r : R} : r ∈ N.colon (Submodule.span R { x }) ↔ r • x ∈ N :=
  calc
    r ∈ N.colon (Submodule.span R { x }) ↔ ∀ a : R, r • a • x ∈ N := by
      simp [Submodule.mem_colon, Submodule.mem_span_singleton]
    _ ↔ r • x ∈ N := by simp_rw [fun (a : R) ↦ smul_comm r a x]; exact SetLike.forall_smul_mem_iff

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