mem_mapSubmodule_apply — Mathlib

English

Membership in mapSubmodule corresponds to membership under of R M a.

Русский

Членство в mapSubmodule соответствует членству в p через of.

LaTeX

$$$m \in mapSubmodule R M a p \iff (of R M a)^{-1} m \in p$$$

Lean4

@[simp]
theorem mem_mapSubmodule_apply {p : (Algebra.lsmul R R M a).invtSubmodule} {m : AEval R M a} :
    m ∈ mapSubmodule R M a p ↔ (of R M a).symm m ∈ (p : Submodule R M) :=
  ⟨fun ⟨_, hm, hm'⟩ ↦ hm'.symm ▸ hm, fun hm ↦ ⟨(of R M a).symm m, hm, rfl⟩⟩

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