toBitVec_nsmul — Mathlib

English

Let n be a natural number and a a 32-bit unsigned integer. Then the 32-bit bit-vector of n times a equals n times the 32-bit bit-vector of a.

Русский

Пусть n — натуральное число и a — UInt32. 32-битный битовый вектор n·a равен n·(битовый вектор a).

LaTeX

$$$$ \forall n \in \mathbb{N}, \forall a \in \mathrm{UInt32},\quad (n a)^{\text{bv}_{32}} = n \cdot a^{\text{bv}_{32}}. $$$$

Lean4

protected theorem toBitVec_nsmul (n : ℕ) (a : UInt32) : (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

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