map_sub_int' — Mathlib

English

For AddGroupWithOne G and AddGroup H with AddConstMapClass F G H 1 b, for any f and x and integer n, f(x − n) = f(x) − n·b.

Русский

Для AddGroupWithOne G и AddGroup H и AddConstMapClass F G H 1 b: для любого f, x и целого n: f(x − n) = f(x) − n·b.

LaTeX

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

Lean4

@[scoped simp]
theorem map_sub_int' [AddGroupWithOne G] [AddGroup H] [AddConstMapClass F G H 1 b] (f : F) (x : G) (n : ℤ) :
    f (x - n) = f x - n • b := by rw [← map_sub_zsmul, zsmul_one]

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