bit_div_two

Mathlib.Data.Nat.BinaryRec

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

← MathLib Explorer

English

Let b ∈ {true, false} and n ∈ ℕ. Then bit b n / 2 = n.

Русский

Пусть b ∈ {true, false} и n ∈ ℕ. Тогда bit b n / 2 = n.

LaTeX

$$$\forall b \in \{\\text{true},\\text{false}\\}, \forall n \in \mathbb{N}, bit(b,n)/2 = n$$$

Lean4

@[simp]
theorem bit_div_two (b n) : bit b n / 2 = n :=
  by
  rw [bit_val, Nat.add_comm, add_mul_div_left, div_eq_of_lt, Nat.zero_add]
  · cases b <;> decide
  · decide

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

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

Разделы

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

Аффилиация

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