toZModSubmodule — Mathlib

English

Reinterpret an additive subgroup as a ZMod-submodule via the ZMod action.

Русский

Переинтерпретировать аддитивную подгруппу как ZMod-подмодуль через действие ZMod.

LaTeX

$$$\\text{toZModSubmodule}(L) : AddSubgroup M \\simeq_o Submodule(ZMod n) M$$$

Lean4

/-- Reinterpret an additive subgroup of a `ℤ/nℤ`-module as a `ℤ/nℤ`-submodule.

See also: `AddSubgroup.toIntSubmodule`, `AddSubmonoid.toNatSubmodule`. -/
def toZModSubmodule : AddSubgroup M ≃o Submodule (ZMod n) M
    where
  toFun S := { S with smul_mem' := fun c _ h ↦ ZMod.smul_mem (K := S) h c }
  invFun := Submodule.toAddSubgroup
  map_rel_iff' := Iff.rfl

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