English
Let z be any integer and a any 8-bit unsigned integer. The 8-bit bit-vector of the product z·a equals z times the 8-bit bit-vector of a; i.e., the bit-vector encoding commutes with integer scaling.
Русский
Пусть z — произвольное целое число и a — произвольное 8-битное беззнаковое число. 8-битный битовый вектор произведения z·a равен z, умноженному на 8-битный битовый вектор a; то есть кодировка битового вектора commuting с целочисленным умножением.
LaTeX
$$$$ \forall z \in \mathbb{Z}, \forall a \in \mathrm{UInt8},\quad \mathrm{bv}_8(z a) = z \cdot \mathrm{bv}_8(a). $$$$
Lean4
@[simp, int_toBitVec]
protected theorem toBitVec_zsmul (z : ℤ) (a : UInt8) : (z • a).toBitVec = z • a.toBitVec :=
by
change (z * a).toBitVec = BitVec.ofInt _ z * a.toBitVec
rw [toBitVec_mul]
congr 1
rw [toBitVec_intCast]
rfl
