cast_bit0 — Mathlib

English

For any α with AddGroupWithOne, (n.bit0 : α) = (n : α) + n.

Русский

Для любого α с AddGroupWithOne: (n.bit0 : α) = (n : α) + n.

LaTeX

$$$$\forall n:\mathrm{ZNum},\ (n.\text{bit0} : \alpha) = (n : \alpha) + n.$$$$

Lean4

@[simp, norm_cast]
theorem cast_bit0 [AddGroupWithOne α] : ∀ n : ZNum, (n.bit0 : α) = (n : α) + n
  | 0 => (add_zero _).symm
  | pos p => by rw [ZNum.bit0, cast_pos, cast_pos]; rfl
  | neg p => by rw [ZNum.bit0, cast_neg, cast_neg, PosNum.cast_bit0, neg_add_rev]

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