toIntSubmodule — Mathlib

English

An additive subgroup of M corresponds to a ℤ-submodule of M via a natural order isomorphism.

Русский

Аддитивная подгруппа M эквивалентна ℤ-подмодулю M через естественное порядковое изоморфизм.

LaTeX

$$$\\text{toIntSubmodule} : AddSubgroup M \\cong_o Submodule \\mathbb{Z} M$$$

Lean4

/-- An additive subgroup is equivalent to a ℤ-submodule. -/
def toIntSubmodule : AddSubgroup M ≃o Submodule ℤ M
    where
  toFun S := { S with smul_mem' := fun _ _ hs ↦ S.zsmul_mem hs _ }
  invFun := Submodule.toAddSubgroup
  map_rel_iff' := Iff.rfl

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