hyperoperation_three

Mathlib.Data.Nat.Hyperoperation

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

English

Let m,k ∈ ℕ. The third hyperoperation equals exponentiation: H3(m,k) = m^k.

Русский

Пусть m,k ∈ ℕ. Третья гипероперация равна возведению в степень: H3(m,k) = m^k.

LaTeX

$$$\\forall m,k \\in \\mathbb{N}, \\ H_3(m,k) = m^k$$$

Lean4

@[simp, grind =]
theorem hyperoperation_three (m k : ℕ) : hyperoperation 3 m k = m ^ k := by induction k with grind

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

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

Разделы

Аффилиация

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