mulVecLin_one — Mathlib

English

The mulVecLin map sends the identity matrix to the identity linear map.

Русский

Матрица-единица переобразуется линейным отображением-идентичностью под mulVecLin.

LaTeX

$$[DecidableEq n] : Matrix.mulVecLin (1 : Matrix n n R) = LinearMap.id$$

Lean4

@[simp]
theorem mulVecLin_one [DecidableEq n] : Matrix.mulVecLin (1 : Matrix n n R) = LinearMap.id := by ext;
  simp [Matrix.one_apply, Pi.single_apply, eq_comm]

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