ofMatrix — Mathlib

English

There is an equivalence of matrices and CStarMatrix: ofMatrix : Matrix m n A ≃ CStarMatrix m n A.

Русский

Существует эквивалентность между матрицами и CStarMatrix: ofMatrix : Matrix m n A ≃ CStarMatrix m n A.

LaTeX

$$$ \text{ofMatrix} : \mathrm{Matrix}_{m,n}(A) \simeq \mathrm{CStarMatrix}_{m,n}(A) $$$

Lean4

/-- The equivalence between `Matrix m n A` and `CStarMatrix m n A`. -/
def ofMatrix {m n A : Type*} : Matrix m n A ≃ CStarMatrix m n A :=
  Equiv.refl _

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