toBitVec_zsmul — Mathlib

English

The bit-vector of a Z-module scalar multiple respects smul: (z • a).toBitVec = z • a.toBitVec.

Русский

Битовому вектору произведения по целочислённому умножению соответствует умножение битного вектора на z.

LaTeX

$$$\forall z\in\mathbb{Z},\; \forall a\in\mathrm{USize},\; (z \cdot a).\operatorname{toBitVec} = z \cdot a.\operatorname{toBitVec}$$$

Lean4

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

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