apply_int — Mathlib

English

Let f: Z →+ β be an additive group homomorphism to an additive group β. Then for every integer n, f(n) = n · f(1).

Русский

Пусть f: ℤ →+ β — аддитивный гомоморфизм в аддитивную группу β. Тогда для каждого целого числа n выполняется f(n) = n · f(1).

LaTeX

$$$\\forall f:\\mathbb{Z}\\to_+\\beta\\ ,\\ \\forall n\\in\\mathbb{Z},\\ f(n)=n\\cdot f(1)$$$

Lean4

theorem apply_int (f : ℤ →+ β) (n : ℤ) : f n = n • f 1 := by
  rw [← zmultiplesHom_symm_apply, ← zmultiplesHom_apply, Equiv.apply_symm_apply]

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