toIntSubmodule_toAddSubgroup — Mathlib

English

For a ring R, a submodule N of M corresponds, via restriction to ℤ, to the same additive subgroup.

Русский

Для кольца R подмодуль N ⊆ M соответствуют через ограничение к ℤ той же аддитивной подгруппе.

LaTeX

$$$$ N^{\\mathbb{Z}} = N.\\restrictionScalars \\mathbb{Z}.$$$$

Lean4

@[simp]
theorem toIntSubmodule_toAddSubgroup {R M : Type*} [Ring R] [AddCommGroup M] [Module R M] (N : Submodule R M) :
    N.toAddSubgroup.toIntSubmodule = N.restrictScalars ℤ :=
  rfl

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