map_int_add' — Mathlib

English

If G is AddCommGroupWithOne and f ∈ AddConstMapClass F G H 1 b, then for natural n, f(n + x) = f(x) + n·b.

Русский

Если G имеет AddCommGroupWithOne и f ∈ AddConstMapClass F G H 1 b, то для натурального n: f(n + x) = f(x) + n·b.

LaTeX

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

Lean4

@[scoped simp]
theorem map_int_add' [AddCommGroupWithOne G] [AddGroup H] [AddConstMapClass F G H 1 b] (f : F) (n : ℤ) (x : G) :
    f (↑n + x) = f x + n • b := by rw [← map_zsmul_add, zsmul_one]

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