toBitVec_zsmul — Mathlib

English

For any integer z and any UInt16 a, the 16-bit bit-vector of z times a equals z times the 16-bit bit-vector of a.

Русский

Пусть z — целое число и a — UInt16. 16-битный битовый вектор z·a равен z умноженному на битовый вектор a.

LaTeX

$$$$ \forall z \in \mathbb{Z}, \forall a \in \mathrm{UInt16},\quad (z \cdot a)^{\text{bv}_{16}} = z \cdot a^{\text{bv}_{16}}. $$$$

Lean4

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

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