toIntSubmodule_closure — Mathlib

English

For any subset s of a module M over a ring R, the additive subgroup closure of s, viewed as a Z-submodule, is exactly the Z-span of s.

Русский

Для любого подмножества s модуля M над кольцом R аддитивное замыкание s равно Z-спану s.

LaTeX

$$$\langle s \rangle_{\mathbb{Z}} = \operatorname{span}_{\mathbb{Z}}(s)$$$

Lean4

theorem _root_.AddSubgroup.toIntSubmodule_closure (s : Set M) : (AddSubgroup.closure s).toIntSubmodule = .span ℤ s :=
  (Submodule.span_le.mpr AddSubgroup.subset_closure).antisymm'
    ((Submodule.span ℤ s).toAddSubgroup.closure_le.mpr Submodule.subset_span)

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