English
There is an algebra isomorphism MopMatrix between matrix algebras over αᵒᵖ and the opposite of the matrix algebra over α, realized by transpose combined with opposite.
Русский
Существует алгебраическое изоморфизм MopMatrix между матричными алгебрами над αᵒᵖ и противоположной матричной алгеброй над α, реализованный транспонированием и операцией противоположности.
LaTeX
$$$\text{mopMatrix}: \mathrm{Mat}_{m\times m}(\alpha^{\mathrm{op}}) \cong (\mathrm{Mat}_{m\times m}(\alpha))^{\mathrm{op}}$$$
Lean4
/-- For any algebra `α` over a ring `R`, we have an `R`-algebra isomorphism
`Matₙₓₙ(αᵒᵖ) ≅ (Matₙₓₙ(R))ᵒᵖ` given by transpose. If `α` is commutative,
we can get rid of the `ᵒᵖ` in the left-hand side, see `Matrix.transposeAlgEquiv`. -/
@[simps!]
def mopMatrix : Matrix m m αᵐᵒᵖ ≃ₐ[R] (Matrix m m α)ᵐᵒᵖ
where
__ := RingEquiv.mopMatrix
commutes'
_ := MulOpposite.unop_injective <| by ext; simp [algebraMap_matrix_apply, eq_comm, apply_ite MulOpposite.unop]
