natCast_mulVec — Mathlib

English

For a natural number x, the scalar x acts on a vector v by the same scalar multiplication as in α.

Русский

Для натурального числа x действуем на вектор v как через приведение x к α и скалярное умножение.

LaTeX

$$$\text{ofNat}(x) \cdotᵥ v = (\text{ofNat}(x) : α) \cdot v$$$

Lean4

@[simp]
theorem natCast_mulVec (x : ℕ) (v : m → α) : x *ᵥ v = (x : α) • v :=
  diagonal_const_mulVec _ _

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