English
Let G be an additive abelian group, S a collection of subgroups of G closed under the subgroup operation, and K ∈ S. If G is a module over ZMod n, then the scalar action of ZMod n on G restricts to K; i.e., for every a ∈ ZMod n and every x ∈ K, we have a • x ∈ K.
Русский
Пусть G — абелева группа, S — множество подгрупп G, замкнутое относительно операции взятия подгруппы, и K ∈ S. Если G является модулем над ZMod n, то действие скаляров ZMod n на G ограничено на K; то есть для любого a ∈ ZMod n и любого x ∈ K выполняется a • x ∈ K.
LaTeX
$$$\forall a \in \mathbb{Z}/n\mathbb{Z},\ \forall x \in K:\ a \cdot x \in K$$$
Lean4
/-- This cannot be made an instance because of the `[Module (ZMod n) G]` argument and the fact that
`n` only appears in the second argument of `SMulMemClass`, which is an `OutParam`. -/
theorem smulMemClass : SMulMemClass S (ZMod n) G where smul_mem _ _ {_x} hx := zmod_smul_mem hx _
