mod_self_nsmul — Mathlib

English

For s ∈ ℕ and x ∈ A[n], s·x = (s mod n)·x; i.e., scalar multiplication by s on the n-torsion subgroup factors through the remainder modulo n.

Русский

Для s ∈ ℕ и x ∈ A[n], s·x = (s mod n)·x; умножение на s в n-тормионной подпгруппе факторизуется через остаток от деления на n.

LaTeX

$$$s\\,\\cdot x = (s \\bmod n)\\,\\cdot x \\quad \\text{для всех } x \\in A[n]$$$

Lean4

theorem mod_self_nsmul (s : ℕ) (x : A[n]) : s • x = (s % n) • x :=
  nsmul_eq_mod_nsmul s (torsionBy.nsmul x)

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