instZModModule — Mathlib

English

A subgroup K of G that is closed under the AddSubgroupClass inherits a Module structure over ZMod n from G via the subtype construction.

Русский

Подмножество K подгруппы G, замкнутое относительно AddSubgroupClass, наследует структуру модуля над ZMod n от G через отбивку подмодуля.

LaTeX

$$$Module(\mathbb{Z}/n\mathbb{Z})K$$$

Lean4

instance instZModModule : Module (ZMod n) K :=
  fast_instance%Subtype.coe_injective.module _ (AddSubmonoidClass.subtype K) coe_zmod_smul

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