map_add_nsmul — Mathlib

English

Under the same assumptions, for all f ∈ F, x ∈ G and n ∈ ℕ, one has f(x + n·a) = f(x) + n·b, i.e., translation by n·a corresponds to translation by n·b under f.

Русский

При тех же допущениях для любых f ∈ F, x ∈ G и n ∈ ℕ выполняется f(x + n·a) = f(x) + n·b, то есть повторное применение переноса на a и на b сохраняется через f.

LaTeX

$$$\\forall f \\in F, \\forall x \\in G, \\forall n \\in \\mathbb{N},\\ f(x + n\\cdot a) = f(x) + n\\cdot b$$$

Lean4

@[scoped simp]
theorem map_add_nsmul [AddMonoid G] [AddMonoid H] [AddConstMapClass F G H a b] (f : F) (x : G) (n : ℕ) :
    f (x + n • a) = f x + n • b := by simpa using (AddConstMapClass.semiconj f).iterate_right n x

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