mem_toSubmodule — Mathlib

English

Let S be a subalgebra of A over R. The elements of the submodule associated to S are exactly the elements of S; membership in the submodule coincides with membership in S.

Русский

Пусть S — подалгебра A над R. Множество подмодуля, связанное с S, состоит ровно из элементов S; принадлежность элементa подмодулю совпадает с принадлежностью элементa S.

LaTeX

$$$\forall x \in A: x \in (toSubmodule\, S) \iff x \in S$$$

Lean4

@[simp]
theorem mem_toSubmodule {x} : x ∈ (toSubmodule S) ↔ x ∈ S :=
  Iff.rfl

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