vecMul_diagonal_const — Mathlib

English

Natural numbers cast to α act on vectors by scalar multiplication; x·ᵥ v equals (x as α) times v.

Русский

Натуральное число, приведённое к α, действует на вектор через скалярное умножение: x·ᵥ v = (x ∙) v.

LaTeX

$$$x \cdotᵥ v = (x \;\text{ как } α) \cdot v$$$

Lean4

@[simp]
theorem vecMul_diagonal_const (x : α) (v : m → α) : v ᵥ* (diagonal fun _ => x) = MulOpposite.op x • v := by ext;
  simp [vecMul_diagonal]

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