toBitVec_intCast — Mathlib

English

For every integer z, the 64-bit bit-vector obtained from z by casting to UInt64 and then to a bit-vector equals z.

Русский

Пусть z — целое число. 64-битный битовый вектор, получаемый приведением z к UInt64 и затем к битовому вектору, равен z.

LaTeX

$$$$ \forall z \in \mathbb{Z},\quad (z \; : \mathrm{UInt64}).toBitVec = z. $$$$

Lean4

@[simp, int_toBitVec]
protected theorem toBitVec_intCast (z : ℤ) : (z : UInt64).toBitVec = z :=
  by
  obtain ⟨z, rfl | rfl⟩ := z.eq_nat_or_neg
  · erw [intCast_ofNat]; rfl
  · rw [intCast_neg, toBitVec_neg]
    erw [intCast_ofNat]
    simp

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