zmodModule — Mathlib

English

If x lies in a subobject K, then any scalar c from ZMod n preserves membership: c•x ∈ K.

Русский

Если x принадлежит подобъекту K, то любое скалярное умножение из ZMod n сохраняет принадлежность: c•x ∈ K.

LaTeX

$$$c\\cdot x \\in K$ for all c ∈ ZMod n whenever x ∈ K$$

Lean4

/-- The quotient of an abelian group by a subgroup containing all multiples of `n` is a
`n`-torsion group. -/
-- See note [reducible non-instances]

abbrev zmodModule {G : Type*} [AddCommGroup G] {H : AddSubgroup G} (hH : ∀ x, n • x ∈ H) : Module (ZMod n) (G ⧸ H) :=
  AddCommGroup.zmodModule <| by simpa [QuotientAddGroup.forall_mk, ← QuotientAddGroup.mk_nsmul]

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