English
Conjugate transpose defines a ring equivalence between square matrices and the opposite ring of matrices, sending M to M^H and preserving multiplication up to the opposite order.
Русский
Сопряжённое транспонирование задаёт кольцевое эквивалентное отображение между квадратными матрицами и противоположным кольцом матриц, отправляя M в M^H и сохраняя умножение в противоположном порядке.
LaTeX
$$$ conjTransposeRingEquiv[m,m,α] : Matrix m m α \cong^+_* (Matrix m m α)^{\text{op}} $$$
Lean4
/-- `Matrix.conjTranspose` as a `RingEquiv` to the opposite ring -/
@[simps]
def conjTransposeRingEquiv [Semiring α] [StarRing α] [Fintype m] : Matrix m m α ≃+* (Matrix m m α)ᵐᵒᵖ :=
{
(conjTransposeAddEquiv m m α).trans
MulOpposite.opAddEquiv with
toFun := fun M => MulOpposite.op Mᴴ
invFun := fun M => M.unopᴴ
map_mul' := fun M N => (congr_arg MulOpposite.op (conjTranspose_mul M N)).trans (MulOpposite.op_mul _ _) }
