diagonal_const_mulVec

Mathlib.Data.Matrix.Mul

URI: https://scilib.ai/kg/mathlib#Matrix.diagonal_const_mulVec

English

Multiplying a vector by a diagonal matrix with constant x multiplies the vector by the scalar x.

Русский

Умножение вектора на диагональную матрицу с константой x даёт результат x·v.

LaTeX

$$$(\text{diagonal} \; (\lambda \cdot) ) \; *ᵥ \, v = x \cdot v$$$

Lean4

@[simp]
theorem diagonal_const_mulVec (x : α) (v : m → α) : (diagonal fun _ => x) *ᵥ v = x • v := by ext; simp [mulVec_diagonal]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru