toAddSubgroup_toIntSubmodule — Mathlib

English

Let S be a Submodule of the abelian group M over the integers. Then taking S to an AddSubgroup and back to a Submodule of M yields S again.

Русский

Пусть S — подмодуль группы M над целыми числами. Приведя S к AddSubgroup и обратно к Submodule, получаем снова S.

LaTeX

$$$S^{\toAddSubgroup\toIntSubmodule} = S$$$

Lean4

theorem toAddSubgroup_toIntSubmodule (S : Submodule ℤ M) : S.toAddSubgroup.toIntSubmodule = S :=
  AddSubgroup.toIntSubmodule.apply_symm_apply S

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