bit_coe_nat — Mathlib

English

For any boolean b and natural n, bit b n equals the natural bit b n cast to an integer.

Русский

Для любого булевого значения b и натурального n бит b n равно натуральному биту b n, приведённому к целому числу.

LaTeX

$$$$ \operatorname{bit}(b,n) = \operatorname{natCast}(\operatorname{Nat.bit}(b,n)). $$$$

Lean4

@[simp]
theorem bit_coe_nat (b) (n : ℕ) : bit b n = Nat.bit b n :=
  by
  rw [bit_val, Nat.bit_val]
  cases b <;> rfl

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