vecMul_ofNat — Mathlib

English

Multiplying a vector by a natural number is the same as scalar multiplying by its α-cast.

Русский

Умножение вектора на натуральное число равно скаляру умножению на соответствующий элемент α.

LaTeX

$$$v ᵥ* ofNat(x) = (ofNat(x) : α) \cdot v$$$

Lean4

@[simp]
theorem vecMul_ofNat (x : ℕ) [x.AtLeastTwo] (v : m → α) : v ᵥ* ofNat(x) = MulOpposite.op (OfNat.ofNat x : α) • v :=
  vecMul_natCast _ _

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