English
For any natural number n and any 16-bit unsigned integer a, the 16-bit bit-vector of n times a equals n times the 16-bit bit-vector of a; the bit-vector encoding is compatible with natural scalar multiplication.
Русский
Пусть n — натуральное число, a — 16-битное беззнаковое число. 16-битный битовый вектор произведения n на a равен n, умноженному на 16-битный битовый вектор a.
LaTeX
$$$$ \forall n \in \mathbb{N}, \forall a \in \mathrm{UInt16},\quad (n a)^{\text{bv}_{16}} = n \cdot a^{\text{bv}_{16}}. $$$$
Lean4
protected theorem toBitVec_nsmul (n : ℕ) (a : UInt16) : (n • a).toBitVec = n • a.toBitVec :=
by
rw [Lean.Grind.Semiring.nsmul_eq_natCast_mul, toBitVec_mul, nsmul_eq_mul, BitVec.natCast_eq_ofNat]
rfl
