div2_bit

Mathlib.Data.Nat.Bits

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

← MathLib Explorer

English

div2(bit b n) = n for any Bool b and natural n.

Русский

div2(bit(b,n)) = n для любого булева b и натурального n.

LaTeX

$$$$ \forall (b : \mathrm{Bool}) (n : \mathbb{N}), \; \mathrm{div2}(\mathrm{bit}(b,n)) = n. $$$$

Lean4

@[simp, grind =]
theorem div2_bit (b n) : div2 (bit b n) = n := by
  rw [bit_val, div2_val, Nat.add_comm, add_mul_div_left, div_eq_of_lt, Nat.zero_add] <;> cases b <;> decide

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

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

Разделы

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

Аффилиация

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