smul_eq_mul_diagonal

Mathlib.Data.Matrix.Mul

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

English

For a finite index set and any matrix M and scalar a, a · M = M · diag(a).

Русский

Для конечного множества индексов и любой матрицы M и скаляра a выполнено a · M = M · diag(a).

LaTeX

$$a\\cdot M = M\\cdot \\mathrm{diag}(a)$$

Lean4

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

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

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

Разделы

Аффилиация

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