English
There is an algebra isomorphism MopMatrix between matrix algebras over αᵒᵖ and the opposite of the matrix algebra over α, realized by transpose and op maps.
Русский
Существует алгебраическое изоморфизм MopMatrix между матричными алгебрами над αᵒᵖ и противоположной алгеброй матричной алгебры над α, реализованный транспонированием и операциями opposite.
LaTeX
$$$\text{mopMatrix}: \mathrm{Mat}_{m\times m}(\alpha^{\mathrm{op}}) \cong\!\!\mathrm{Mat}_{m\times m}(\alpha)^{\mathrm{op}}$$$
Lean4
/-- For any ring `R`, we have ring isomorphism `Matₙₓₙ(Rᵒᵖ) ≅ (Matₙₓₙ(R))ᵒᵖ` given by transpose.
-/
@[simps apply symm_apply]
def mopMatrix : Matrix m m αᵐᵒᵖ ≃+* (Matrix m m α)ᵐᵒᵖ
where
toFun M := op (M.transpose.map unop)
invFun M := M.unop.transpose.map op
left_inv _ := by aesop
right_inv _ := by aesop
map_mul' _ _ := unop_injective <| by ext; simp [transpose, mul_apply]
map_add' _ _ := by aesop
