bodd_bit — Mathlib

English

For any Bool b and natural n, bodd(bit b n) = b.

Русский

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

LaTeX

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

Lean4

@[simp, grind =]
theorem bodd_bit (b n) : bodd (bit b n) = b := by
  rw [bit_val]
  simp only [Nat.mul_comm, Nat.add_comm, bodd_add, bodd_mul, bodd_succ, bodd_zero, Bool.not_false, Bool.not_true,
    Bool.and_false, Bool.xor_false]
  cases b <;> cases bodd n <;> rfl

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