English
There is a canonical star-linear equivalence between the space of m×n matrices and the space of n×m matrices, given by the conjugate transpose, i.e., conjTranspose defines a star-linear equivalence M: Matrix m n α → Matrix n m α with inverse given by conjTranspose.
Русский
Существует каноническое звёздочно-линейное эквивалентное преобразование между пространством матриц размером m×n и пространством матриц размером n×m, задаваемое сопряжённым транспонированием: conjTranspose задаёт звёздно-линейное эквивалентное отображение.
LaTeX
$$$ conjTransposeLinearEquiv: Matrix m n α \ \text{сложимо }\; Matrix n m α, \quad \text{toFun}(M) = M^H, \text{invFun}(N) = N^H $$$
Lean4
/-- `Matrix.conjTranspose` as a `LinearMap` -/
@[simps apply]
def conjTransposeLinearEquiv [CommSemiring R] [StarRing R] [AddCommMonoid α] [StarAddMonoid α] [Module R α]
[StarModule R α] : Matrix m n α ≃ₗ⋆[R] Matrix n m α :=
{ conjTransposeAddEquiv m n α with map_smul' := conjTranspose_smul }
