mem_toSubmodule — Mathlib

English

For any S, an element x of A lies in the submodule S.toSubmodule if and only if x lies in S itself.

Русский

Для любой подпалгебры S элемент x принадлежит подмодулю S.toSubmodule тогда и только тогда, когда он принадлежит самому S.

LaTeX

$$$\forall S \in \text{NonUnitalSubalgebra}(R,A),\; x \in S.toSubmodule \iff x \in S$$$

Lean4

theorem mem_toSubmodule (S : NonUnitalSubalgebra R A) {x} : x ∈ S.toSubmodule ↔ x ∈ S :=
  Iff.rfl

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