map_add_ofNat' — Mathlib

English

Let ofNat(n) denote the natural-number embedding in G. Then for all f ∈ F, x ∈ G and n ∈ ℕ with n ≥ 2, f(x + ofNat(n)) = f(x) + ofNat(n) · b.

Русский

Пусть ofNat(n) обозначает вложение натурального числа в G. Тогда для всех f ∈ F, x ∈ G и n ∈ ℕ с n ≥ 2 выполняется f(x + ofNat(n)) = f(x) + ofNat(n)·b.

LaTeX

$$$\\forall f \\in F, \\forall x \\in G, \\forall n \\in \\mathbb{N},\\ [n\\ge 2] \\Rightarrow f(x + \\operatorname{ofNat}(n)) = f(x) + \\operatorname{ofNat}(n)\\,b$$$

Lean4

@[scoped simp]
theorem map_add_ofNat' [AddMonoidWithOne G] [AddMonoid H] [AddConstMapClass F G H 1 b] (f : F) (x : G) (n : ℕ)
    [n.AtLeastTwo] : f (x + ofNat(n)) = f x + (ofNat(n) : ℕ) • b :=
  map_add_nat' f x n

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