English
The operation conjTransposeAddEquiv provides an additive equivalence between matrices of size m×n and those of size n×m, with conjTranspose as the forward and inverse map.
Русский
Операция conjTransposeAddEquiv образует аддитивное эквивалентное отображение между матрицами размера m×n и размером n×m, где сопряжённое транспонирование служит прямым и обратным отображением.
LaTeX
$$$ conjTransposeAddEquiv\, m\, n\, α : (Matrix\, m\, n\, α) \simeq_{Add} (Matrix\, n\, m\, α),\quad toFun = M \mapsto M^H,\; invFun = N \mapsto N^H $$$
Lean4
/-- `Matrix.conjTranspose` as an `AddEquiv` -/
@[simps apply]
def conjTransposeAddEquiv [AddMonoid α] [StarAddMonoid α] : Matrix m n α ≃+ Matrix n m α
where
toFun := conjTranspose
invFun := conjTranspose
left_inv := conjTranspose_conjTranspose
right_inv := conjTranspose_conjTranspose
map_add' := conjTranspose_add
