zero_bits

Mathlib.Data.Nat.Bits

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

English

bits(0) = [].

Русский

bits(0) = [].

LaTeX

$$$$ \text{bits}(0) = []. $$$$

Lean4

@[simp]
theorem zero_bits : bits 0 = [] := by simp [Nat.bits]

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

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

Разделы

Аффилиация

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