English
Let a map f belong to a family that sends x + 1_G to f(x) + b in the codomain, for fixed a = 1_G and b. Then for every x in G and every natural number n with n ≥ 2, f(x − n·1_G) = f(x) − n·b.
Русский
Пусть f принадлежит классу отображений, удовлетворяющему f(x + 1_G) = f(x) + b для фиксированного a = 1_G и фиксированного b в H. Тогда для любого x ∈ G и любого натурального n ≥ 2 выполняется f(x − n·1_G) = f(x) − n·b.
LaTeX
$$$ f(x - n \cdot 1_G) = f(x) - n \cdot b \quad \text{for all } x \in G,\ n \in \mathbb{N},\ n \ge 2. $$$
Lean4
@[scoped simp]
theorem map_sub_ofNat' [AddGroupWithOne G] [AddGroup H] [AddConstMapClass F G H 1 b] (f : F) (x : G) (n : ℕ)
[n.AtLeastTwo] : f (x - ofNat(n)) = f x - ofNat(n) • b :=
map_sub_nat' f x n
