map_add_int — Mathlib

English

Let f be in AddConstMapClass with a = 1_G and b = 1_H. Then for any integer n and x in G, f(x + n) = f(x) + n.

Русский

Пусть f относится к AddConstMapClass с a = 1_G и b = 1_H. Тогда для любого n ∈ ℤ и x ∈ G выполняется f(x + n) = f(x) + n.

LaTeX

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

Lean4

theorem map_add_int [AddGroupWithOne G] [AddGroupWithOne H] [AddConstMapClass F G H 1 1] (f : F) (x : G) (n : ℤ) :
    f (x + n) = f x + n := by simp

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