mulRightLinearMap_one — Mathlib

English

Right multiplication by the identity matrix yields the identity operator.

Русский

Правое умножение на единичную матрицу даёт тождественное отображение.

LaTeX

$$$\operatorname{mulRightLinearMap} l\ R\ (I_m) = \mathrm{Id}$$$

Lean4

/-- A version of `LinearMap.mulRight_one` for matrix multiplication. -/
@[simp]
theorem mulRightLinearMap_one : mulRightLinearMap l R (1 : Matrix m m A) = LinearMap.id :=
  LinearMap.ext fun _ => Matrix.mul_one _

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