hyperoperation_two

Mathlib.Data.Nat.Hyperoperation

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

English

Let m,n ∈ ℕ. The second hyperoperation coincides with ordinary multiplication: H2(m,n) = m·n.

Русский

Пусть m,n ∈ ℕ. Вторая гипероперация совпадает с обычным умножением: H2(m,n) = m·n.

LaTeX

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

Lean4

@[simp, grind =]
theorem hyperoperation_two (m k : ℕ) : hyperoperation 2 m k = m * k := by induction k with grind

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

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

Разделы

Аффилиация

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