smul_eq_diagonal_mul

Mathlib.Data.Matrix.Mul

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

English

Let d1, d2 : n → α. Then diag(d1) · diag(d2) = diag(i ↦ d1(i) d2(i)).

Русский

Пусть d1, d2 : n → α. Тогда diag(d1) diag(d2) = diag(i ↦ d1(i) d2(i)).

LaTeX

$$$\\operatorname{diagonal}(d_1) \\cdot \\operatorname{diagonal}(d_2) = \\operatorname{diagonal}(i \\mapsto d_1(i) \\cdot d_2(i))$$$

Lean4

theorem smul_eq_diagonal_mul [Fintype m] [DecidableEq m] (M : Matrix m n α) (a : α) :
    a • M = (diagonal fun _ => a) * M := by
  ext
  simp

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

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

Разделы

Аффилиация

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