vecMul_natCast — Mathlib

English

A vector multiplied by a natural cast (natCast) corresponds to scalar multiplication of the vector by the corresponding α-element.

Русский

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

LaTeX

$$$v \; ᵥ* x^{\mathrm{cast}} = (x^{\mathrm{cast}}) \cdot v$$$

Lean4

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

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