map_zsmul_const — Mathlib

English

Let f be a constant-translation map as above. Then for every integer n, f(n·a) = f(0) + n·b.

Русский

Пусть f — отображение с постоянным сдвигом; тогда для любого целого числа n выполняется f(n·a) = f(0) + n·b.

LaTeX

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

Lean4

@[scoped simp]
theorem map_zsmul_const [AddGroup G] [AddGroup H] [AddConstMapClass F G H a b] (f : F) (n : ℤ) :
    f (n • a) = f 0 + n • b := by simpa using map_add_zsmul f 0 n

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