and_two_pow — Mathlib

English

For any n and i, n &&& 2^i = (n.testBit i).toNat · 2^i.

Русский

Для любых n и i выполняется n &&& 2^i = (n.testBit i).toNat · 2^i.

LaTeX

$$$ n &&& 2^i = (n.testBit i).toNat \cdot 2^i $$$

Lean4

theorem and_two_pow (n i : ℕ) : n &&& 2 ^ i = (n.testBit i).toNat * 2 ^ i :=
  by
  refine eq_of_testBit_eq fun j => ?_
  obtain rfl | hij := Decidable.eq_or_ne i j <;> cases h : n.testBit i
  · simp [h]
  · simp [h]
  · simp [testBit_two_pow_of_ne hij]
  · simp [testBit_two_pow_of_ne hij]

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