cast_bitm1 — Mathlib

English

For any α with AddGroupWithOne, (n.bitm1 : α) = (n : α) + n − 1.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem cast_bitm1 [AddGroupWithOne α] (n : ZNum) : (n.bitm1 : α) = (n : α) + n - 1 :=
  by
  conv =>
    lhs
    rw [← zneg_zneg n]
  rw [← zneg_bit1, cast_zneg, cast_bit1]
  have : ((-1 + n + n : ℤ) : α) = (n + n + -1 : ℤ) := by simp [add_comm]
  simpa [sub_eq_add_neg] using this

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