cast_bit0 — Mathlib

English

For any α with a non-associative semiring structure, the bit0 operation on Num corresponds to doubling in α: (n.bit0 : α) = 2 * (n : α).

Русский

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

LaTeX

$$$((n.bit0) : \alpha) = 2 \cdot (n : \alpha)$$$

Lean4

@[simp, norm_cast]
theorem cast_bit0 [NonAssocSemiring α] (n : Num) : (n.bit0 : α) = 2 * (n : α) := by
  rw [← bit0_of_bit0, two_mul, cast_add]

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