map_int_add — Mathlib

English

Let f be the AddConstMapClass map with a = 1_G and b = 1_H. Then for all integers n and x, f(n + x) = f(x) + n.

Русский

Пусть f относится к AddConstMapClass с a = 1_G и b = 1_H. Тогда для всех целых n и x: f(n + x) = f(x) + n.

LaTeX

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

Lean4

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

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