hyperoperation_zero

Mathlib.Data.Nat.Hyperoperation

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

English

For all m,k in N, hyperoperation 0 m k = k+1.

Русский

Для любых m,k в натуралах hyperoperation 0 m k = k+1.

LaTeX

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

Lean4

@[simp, grind =]
theorem hyperoperation_zero (m k : ℕ) : hyperoperation 0 m k = k + 1 := by grind

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

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

Разделы

Аффилиация

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