toBitVec_intCast — Mathlib

English

For every integer z, the 16-bit bit-vector obtained by casting z to UInt16 and then to a bit-vector equals z.

Русский

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

LaTeX

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

Lean4

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

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