map_nsmul_add — Mathlib

English

For f ∈ F, n ∈ ℕ and x ∈ G, f(n•a + x) = f(x) + n•b, i.e., n-fold translation commutes with f.

Русский

Для f ∈ F, n ∈ ℕ и x ∈ G выполняется f(n•a + x) = f(x) + n•b.

LaTeX

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

Lean4

@[scoped simp]
theorem map_nsmul_add [AddCommMonoid G] [AddMonoid H] [AddConstMapClass F G H a b] (f : F) (n : ℕ) (x : G) :
    f (n • a + x) = f x + n • b := by rw [add_comm, map_add_nsmul]

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