nat_mul

Mathlib.Computability.Primrec

URI: https://scilib.ai/kg/mathlib#Primrec.nat_mul

English

Multiplication on natural numbers is Primrec₂.

Русский

Умножение натуральных чисел является Primrec₂.

LaTeX

$$$ Primrec_2 ( (\\cdot) \\times (\\cdot) )$$$

Lean4

theorem nat_mul : Primrec₂ ((· * ·) : ℕ → ℕ → ℕ) :=
  Primrec₂.unpaired'.1 Nat.Primrec.mul

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

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

Разделы

Аффилиация

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