toAddSubgroup_toZModSubmodule — Mathlib

English

For a Submodule S of ZMod n-module M, the Submodule obtained from its underlying AddSubgroup is S again.

Русский

Для подмодуля S над ZMod n-модулем M подмодуль, полученный по его базовой AddSubgroup, возвращает S.

LaTeX

$$$(toZModSubmodule(n)\\,S).toAddSubgroup = S$$$

Lean4

@[simp]
theorem _root_.Submodule.toAddSubgroup_toZModSubmodule (S : Submodule (ZMod n) M) :
    toZModSubmodule n S.toAddSubgroup = S :=
  rfl

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