map_add_int' — Mathlib

English

If f belongs to the constant-translation class with a fixed a and b, then for all x in G and all integers n, f(x + n) = f(x) + n·b.

Русский

Если f относится к классу отображений с константным сдвигом и фиксированными a и b, то для любого x ∈ G и любого целого числа n выполняется f(x + n) = f(x) + n·b.

LaTeX

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

Lean4

@[scoped simp]
theorem map_add_int' [AddGroupWithOne G] [AddGroup H] [AddConstMapClass F G H 1 b] (f : F) (x : G) (n : ℤ) :
    f (x + n) = f x + n • b := by rw [← map_add_zsmul f x n, zsmul_one]

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