map_sub_int — Mathlib

English

Under AddConstMapClass with a = 1_G and b = 1_H, for all f, x and integer n, f(x − n) = f(x) − n.

Русский

При AddConstMapClass с a = 1_G и b = 1_H: для всех f, x и целого n выполняется 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_sub_int [AddGroupWithOne G] [AddGroupWithOne H] [AddConstMapClass F G H 1 1] (f : F) (x : G) (n : ℤ) :
    f (x - n) = f x - n := by simp

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