map_add_nat' — Mathlib

English

Under the same assumptions, for all f ∈ F, x ∈ G and n ∈ ℕ, f(x + n·a) = f(x) + n·b, i.e., the n-times translation property holds.

Русский

При тех же предположениях для всех f ∈ F, x ∈ G и n ∈ ℕ выполняется f(x + n·a) = f(x) + n·b.

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_nat' [AddMonoidWithOne G] [AddMonoid H] [AddConstMapClass F G H 1 b] (f : F) (x : G) (n : ℕ) :
    f (x + n) = f x + n • b := by simp [← map_add_nsmul]

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