bit_decide_mod_two_eq_one_shiftRight_one

English

Reconstruct n from its least significant bit and the rest: bit (n mod 2 = 1) (n >>> 1) = n.

Русский

Восстановление n по биту наименее значимого разряда и оставшейся части: bit (n mod 2 = 1) (n >>> 1) = n.

LaTeX

$$$\text{bit}(n \bmod 2 = 1,\; n \\gt 1) = n$$$

Lean4

@[simp]
theorem bit_decide_mod_two_eq_one_shiftRight_one (n : Nat) : bit (n % 2 = 1) (n >>> 1) = n :=
  by
  simp only [bit, shiftRight_one]
  cases mod_two_eq_zero_or_one n with
  | _ h => simpa [h] using Nat.div_add_mod n 2

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