apply_nat

Mathlib.Algebra.Group.Nat.Hom

URI: https://scilib.ai/kg/mathlib#AddMonoidHom.apply_nat

English

For every f: ℕ →+ M and every n ∈ ℕ, f(n) = n • f(1).

Русский

Для каждого f: ℕ →+ M и каждого n ∈ ℕ выполняется f(n) = n • f(1).

LaTeX

$$$ f(n) = n \cdot f(1) $$$

Lean4

theorem apply_nat (f : ℕ →+ M) (n : ℕ) : f n = n • f 1 := by
  rw [← multiplesHom_symm_apply, ← multiplesHom_apply, Equiv.apply_symm_apply]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru