mem_toZModSubmodule

Mathlib.Algebra.Module.ZMod

URI: https://scilib.ai/kg/mathlib#AddSubgroup.mem_toZModSubmodule

English

An element x lies in the ZMod-submodule corresponding to S if and only if x lies in S.

Русский

Элемент x принадлежит соответствующему ZMod-подмодулю S тогда и только тогда, когда x принадлежит S.

LaTeX

$$$x \\in toZModSubmodule(n)\\,S \\;\\Longleftrightarrow\\; x \\in S$$$

Lean4

@[simp]
theorem mem_toZModSubmodule {S : AddSubgroup M} : x ∈ toZModSubmodule n S ↔ x ∈ S :=
  .rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru