toIntSubmodule_toAddSubgroup — Mathlib

English

Let S be an additive subgroup of an additive abelian group M. If we view S inside M as an integer-submodule and then convert it back to an additive subgroup of M, we recover S.

Русский

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

LaTeX

$$$S^{\mathbb Z}_{\toAddSubgroup} = S$$$

Lean4

@[simp]
theorem toIntSubmodule_toAddSubgroup (S : AddSubgroup M) : S.toIntSubmodule.toAddSubgroup = S :=
  AddSubgroup.toIntSubmodule.symm_apply_apply S

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