ofMatrix_eq_ofMatrixL — Mathlib

English

The map ofMatrix coincides with the linear equivalence ofMatrixL on functions; i.e., they are the same identification.

Русский

Отображение ofMatrix совпадает с идентификацией via ofMatrixL, т. е. эти отображения совпадают.

LaTeX

$$$$ (\\mathrm{ofMatrix} : \\mathrm{Matrix}(m,n,A) \\to \\mathrm{CStarMatrix}(m,n,A)) = (\\mathrm{ofMatrixL} : \\mathrm{Matrix}(m,n,A) \\to \\mathrm{CStarMatrix}(m,n,A)). $$$$

Lean4

theorem ofMatrix_eq_ofMatrixL :
    (ofMatrix : Matrix m n A → CStarMatrix m n A) = (ofMatrixL : Matrix m n A → CStarMatrix m n A) :=
  rfl

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