mulLeftLinearMap_one — Mathlib

English

Multiplication on the left by the identity matrix acts as the identity operator.

Русский

Левое умножение на единичную матрицу является тождественным отображением.

LaTeX

$$$\operatorname{mulLeftLinearMap} n\ R\ (I_m) = \mathrm{Id}$$$

Lean4

/-- A version of `LinearMap.mulLeft_one` for matrix multiplication. -/
@[simp]
theorem mulLeftLinearMap_one : mulLeftLinearMap n R (1 : Matrix m m A) = LinearMap.id :=
  LinearMap.ext fun _ => Matrix.one_mul _

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