zmod_smul_mem — Mathlib

English

If x lies in a subobject K, then for every scalar a from ZMod n, the action a • x stays in K; i.e., the ZMod-scaled elements of x remain in K.

Русский

Если x ∈ K, то для каждого скаляра a из ZMod n действие a • x остается в K; т.е. элементы x, умноженные на парциальный скаляр ZMod, остаются в K.

LaTeX

$$$\\text{If } x \\in K \\text{ and } K \\text{ is a } ZMod(n)\\text{-module, then } \\forall a \\in ZMod(n),\\; a \\cdot x \\in K.$$$

Lean4

theorem zmod_smul_mem (hx : x ∈ K) : ∀ a : ZMod n, a • x ∈ K := by
  simpa [ZMod.forall, Int.cast_smul_eq_zsmul] using zsmul_mem hx

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