toBitVec_intCast — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp, int_toBitVec]
protected theorem toBitVec_intCast (z : ℤ) : (z : UInt32).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

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