map_zsmul_add — Mathlib

English

For AddCommGroup G and AddGroup H, with AddConstMapClass F G H a b, we have f(n·a + x) = f(x) + n·b for all integer n and x ∈ G.

Русский

Для G и H с коммутативной группой добавления и AddConstMapClass F G H a b: f(n·a + x) = f(x) + n·b, для любых n∈ℤ и x∈G.

LaTeX

$$$ f(n \cdot a + x) = f(x) + n \cdot b \quad \text{for all } x \in G,\ n \in \mathbb{Z}. $$$

Lean4

@[scoped simp]
theorem map_zsmul_add [AddCommGroup G] [AddGroup 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_zsmul]

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