submoduleOf_span_singleton_of_mem

English

If N ≤ M is a submodule and x ∈ N, then span{x} submoduleOf N equals span{⟨x, hx⟩}.

Русский

Если N ≤ M является подпространством и x ∈ N, то подпространство span{x} в N равно span{⟨x, hx⟩}.

LaTeX

$$$(\operatorname{span} R\{x\}).submoduleOf N = \operatorname{span} R\{\langle x, hx\rangle\}$$$

Lean4

theorem submoduleOf_span_singleton_of_mem (N : Submodule R M) {x : M} (hx : x ∈ N) :
    (span R { x }).submoduleOf N = span R {⟨x, hx⟩} := by
  ext y
  simp_rw [submoduleOf, mem_comap, subtype_apply, mem_span_singleton]
  aesop

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