toBitVec_zsmul — Mathlib

English

For any z ∈ ℤ and a ∈ UInt64, (z • a).toBitVec = z • a.toBitVec.

Русский

Пусть z ∈ ℤ и a ∈ UInt64. (z • a).toBitVec = z • a.toBitVec.

LaTeX

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

Lean4

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

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