cast_bit1 — Mathlib

English

For any α with a non-associative semiring structure, the bit1 operation on Num satisfies (n.bit1 : α) = 2 * (n : α) + 1.

Русский

Для любого α с полугруппой с умножением и единицей, битовая операция bit1 над Num удовлетворяет (n.bit1 : α) = 2 · (n : α) + 1.

LaTeX

$$$((n.bit1) : \alpha) = 2 \cdot (n : \alpha) + 1$$$

Lean4

@[simp, norm_cast]
theorem cast_bit1 [NonAssocSemiring α] (n : Num) : (n.bit1 : α) = 2 * (n : α) + 1 := by
  rw [← bit1_of_bit1, bit0_of_bit0, cast_add, cast_bit0]; rfl

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