toBitVec_nsmul — Mathlib

English

Let n ∈ ℕ and a ∈ UInt64. Then (n • a).toBitVec = n • a.toBitVec.

Русский

Пусть n ∈ ℕ и a ∈ UInt64. Тогда (n • a).toBitVec = n • a.toBitVec.

LaTeX

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

Lean4

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

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