mul_one

Mathlib.Data.Matrix.Mul

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

← MathLib Explorer

English

Multiplying a matrix M on the right by the identity matrix yields M: M · 1 = M.

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

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

Аффилиация

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