map_sub_zsmul — Mathlib

English

For a fixed a ∈ G and b ∈ H, and f in AddConstMapClass, for any x ∈ G and any n ∈ ℤ, f(x − n·a) = f(x) − n·b.

Русский

Пусть f принадлежит AddConstMapClass. Тогда для любых x ∈ G и n ∈ ℤ выполняется f(x − n·a) = f(x) − n·b.

LaTeX

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

Lean4

@[scoped simp]
theorem map_sub_zsmul [AddGroup G] [AddGroup H] [AddConstMapClass F G H a b] (f : F) (x : G) (n : ℤ) :
    f (x - n • a) = f x - n • b := by simpa [sub_eq_add_neg] using map_add_zsmul f x (-n)

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