English
Transpose gives an algebra equivalence between matrices and their opposite algebra structure.
Русский
Транспонирование задаёт алгебраическое эквивалентное отображение между матрицами и их противоположной алгеброй.
LaTeX
$$$\mathrm{transposeAlgEquiv} : \mathrm{Mat}_{m\times m}(\alpha) \cong_\mathsf{Alg} _R (\mathrm{Mat}_{m\times m}(\alpha))^{\mathrm{op}}$ is an AlgEquiv.$$
Lean4
/-- `Matrix.transpose` as a `RingEquiv` to the opposite ring -/
@[simps]
def transposeRingEquiv [AddCommMonoid α] [CommSemigroup α] [Fintype m] : Matrix m m α ≃+* (Matrix m m α)ᵐᵒᵖ :=
{
(transposeAddEquiv 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 (transpose_mul M N)).trans (MulOpposite.op_mul _ _)
left_inv := fun M => transpose_transpose M
right_inv := fun M => MulOpposite.unop_injective <| transpose_transpose M.unop }
