map_add_zsmul — Mathlib

English

Let f be a constant-translation map between additive groups with a fixed a and b. Then for every x in G and every integer n, f(x + n·a) = f(x) + n·b.

Русский

Пусть f — отображение, сохраняющее добавление вплоть до константы, с фиксированными элементами a ∈ G и b ∈ H. Тогда для любого x ∈ G и любого целого числа n выполняется f(x + n·a) = f(x) + n·b.

LaTeX

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

Lean4

@[scoped simp]
theorem map_add_zsmul [AddGroup G] [AddGroup H] [AddConstMapClass F G H a b] (f : F) (x : G) :
    ∀ n : ℤ, f (x + n • a) = f x + n • b
  | (n : ℕ) => by simp
  | .negSucc n => by simp [← sub_eq_add_neg]

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