binaryRec_zero

Mathlib.Data.Nat.BinaryRec

URI: https://scilib.ai/kg/mathlib#Nat.binaryRec_zero

← MathLib Explorer

English

If we evaluate the binary-recursion with the base value at 0, we obtain the base value.

Русский

При вычислении бинарной рекурсии на аргументе 0 получаем базовое значение.

LaTeX

$$$ binaryRec\ (zero)\ (bit)\ 0 = zero $$$

Lean4

@[simp]
theorem binaryRec_zero (zero : motive 0) (bit : ∀ b n, motive n → motive (bit b n)) : binaryRec zero bit 0 = zero :=
  by
  rw [binaryRec]
  simp

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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