mod_self_nsmul' — Mathlib

English

If x ∈ A[n], then s·x = (s mod n)·x for any natural s; a variant of the previous statement.

Русский

Если x ∈ A[n], то s·x = (s mod n)·x для любого натурального s; вариант предыдущего утверждения.

LaTeX

$$$s\\cdot x = (s \\bmod n) \\cdot x$ for all x ∈ A[n]$$

Lean4

theorem mod_self_nsmul' (s : ℕ) {x : A} (h : x ∈ A[n]) : s • x = (s % n) • x :=
  nsmul_eq_mod_nsmul s (torsionBy.nsmul_iff.mp h)

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