English
Let z be any integer. The 8-bit bit-vector corresponding to z, obtained by casting z to an unsigned 8-bit value and then to a bit-vector, equals z viewed as an 8-bit bit-vector; equivalently, it is the residue of z modulo 256.
Русский
Пусть z — произвольное целое число. 8-битный битовый вектор, полученный из z посредством приведения к беззнаковому 8-битному числу и затем к битовому вектору, равен z, рассматриваемому как 8-битный битовый вектор; то есть остаток z по модулю 256.
LaTeX
$$$$ \forall z \in \mathbb{Z},\quad \mathrm{bv}_8(z) = z \bmod 256. $$$$
Lean4
@[simp, int_toBitVec]
protected theorem toBitVec_intCast (z : ℤ) : (z : UInt8).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
