one_mul

Mathlib.Data.Matrix.Mul

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

← MathLib Explorer

English

Multiplying a matrix M on the left by the identity matrix yields M: (1) · M = M.

Русский

Умножение матрицы слева на единичную матрицу даёт ту же матрицу: I · M = M.

LaTeX

$$$ (1_{m}) \\cdot M = M $$$

Lean4

@[simp]
protected theorem one_mul [Fintype m] [DecidableEq m] (M : Matrix m n α) : (1 : Matrix m m α) * M = M :=
  by
  ext
  rw [← diagonal_one, diagonal_mul, one_mul]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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