map_sub_nsmul — Mathlib

English

For additive groups G and H and a fixed a ∈ G, b ∈ H, f(x - n•a) = f(x) - n•b for all n ∈ ℕ.

Русский

Пусть G и H — группы по сложению, фиксированы a ∈ G, b ∈ H. Тогда для любого f ∈ F и x ∈ G и n ∈ ℕ выполняется f(x - n•a) = f(x) - n•b.

LaTeX

$$$\\forall f \\in F,\\forall x \\in G,\\forall n \\in \\mathbb{N}:\\ f(x - n\\cdot a) = f(x) - n\\cdot b$$$

Lean4

@[scoped simp]
theorem map_sub_nsmul [AddGroup G] [AddGroup H] [AddConstMapClass F G H a b] (f : F) (x : G) (n : ℕ) :
    f (x - n • a) = f x - n • b := by conv_rhs => rw [← sub_add_cancel x (n • a), map_add_nsmul, add_sub_cancel_right]

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