div2_bit — Mathlib

English

For a boolean bit and an integer n, the half-division of the binary construction bit b n equals n.

Русский

Для двоичной операции bit и целого n выполняется деление пополам: div2 (bit b n) = n.

LaTeX

$$$\forall b:\text{Bool},\forall n:\mathbb{Z},\ \mathrm{div2}(\mathrm{bit}(b,n)) = n$$$

Lean4

@[simp]
theorem div2_bit (b n) : div2 (bit b n) = n :=
  by
  rw [bit_val, div2_val, add_comm, Int.add_mul_ediv_left, (_ : (_ / 2 : ℤ) = 0), zero_add]
  cases b
  · decide
  · change ofNat _ = _
    rw [Nat.div_eq_of_lt] <;> simp
  · decide

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