testBit_bit_zero — Mathlib

English

The least significant bit of bit b n is b: testBit (bit b n) 0 = b.

Русский

Наименьший значимый бит числа bit b n равен b: testBit (bit b n) 0 = b.

LaTeX

$$$$ \text{testBit}(\operatorname{bit}(b,n),0) = b. $$$$

Lean4

@[simp]
theorem testBit_bit_zero (b) : ∀ n, testBit (bit b n) 0 = b
  | (n : ℕ) => by rw [bit_coe_nat]; apply Nat.testBit_bit_zero
  | -[n+1] => by
    rw [bit_negSucc]; dsimp [testBit]; rw [Nat.testBit_bit_zero]; clear testBit_bit_zero
    cases b <;> rfl

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