binaryRec'_zero

Mathlib.Data.Nat.BinaryRec

URI: https://scilib.ai/kg/mathlib#Nat.binaryRec'_zero

← MathLib Explorer

English

binaryRec' zero bit 0 equals zero.

Русский

binaryRec' ноль bit 0 равно нулю.

LaTeX

$$$ binaryRec'\ zero\ bit\ 0 = zero $$$

Lean4

@[simp]
theorem binaryRec'_zero (zero : motive 0)
    (bit : (b : Bool) → (n : Nat) → (n = 0 → b = true) → motive n → motive (n.bit b)) : binaryRec' zero bit 0 = zero :=
  by rw [binaryRec', Nat.binaryRec_zero]

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

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

Разделы

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

Аффилиация

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