English
Transpose induces a RingEquiv between matrices and their opposite ring structure.
Русский
Транспонирование порождает кольцевой эквивалент между матрицами и их противоположной структурой кольца.
LaTeX
$$$\mathrm{transposeRingEquiv}(m,\alpha) : \mathrm{Mat}_{m\times m}(\alpha) \simeq_\mathrm{Ring} (\mathrm{Mat}_{m\times m}(\alpha))^{\mathrm{op}}$ is a RingEquiv.$$
Lean4
/-- `Matrix.transpose` as an `AlgEquiv` to the opposite ring -/
@[simps]
def transposeAlgEquiv [CommSemiring R] [CommSemiring α] [Fintype m] [DecidableEq m] [Algebra R α] :
Matrix m m α ≃ₐ[R] (Matrix m m α)ᵐᵒᵖ :=
{ (transposeAddEquiv m m α).trans MulOpposite.opAddEquiv,
transposeRingEquiv m α with
toFun := fun M => MulOpposite.op Mᵀ
commutes' := fun r => by simp only [algebraMap_eq_diagonal, diagonal_transpose, MulOpposite.algebraMap_apply] }
