hyperoperation_one

Mathlib.Data.Nat.Hyperoperation

URI: https://scilib.ai/kg/mathlib#hyperoperation_one

English

The first hyperoperation is addition: hyperoperation 1 m k = m + k.

Русский

Первая гипероперация является сложением: hyperoperation 1 m k = m + k.

LaTeX

$$$\forall m,k \in \mathbb{N}, \ hyperoperation(1,m,k) = m + k$$$

Lean4

@[simp, grind =]
theorem hyperoperation_one (m k : ℕ) : hyperoperation 1 m k = m + k := by induction k with grind

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

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

Разделы

Аффилиация

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