chore(Data/Matrix/Basic): mention mopMatrix in transpose{Ring/Alg}Equivs docstring and vice versa (#39123)

- `RingEquiv.mopMatrix` and `transposeRingEquiv` differ by a `ᵐᵒᵖ` since the latter assumes `CommMagma α` instead of `Mul α`
- `AlgEquiv.mopMatrix` and `transposeAlgEquiv` differ by a `ᵐᵒᵖ` since the latter assumes `CommSemiring α` instead of `Semiring α`

Author: SnirBroshi

Mathlib/Data/Matrix/Basic.lean

@@ -639,17 +639,16 @@ theorem mapMatrix_trans (f : α ≃+* β) (g : β ≃+* γ) :
   rfl
 
 open MulOpposite in
-/--
-For any ring `R`, we have ring isomorphism `Matₙₓₙ(Rᵒᵖ) ≅ (Matₙₓₙ(R))ᵒᵖ` given by transpose.
--/
+/-- For any ring `α`, we have ring isomorphism `Matₙₓₙ(αᵒᵖ) ≅ (Matₙₓₙ(α))ᵒᵖ` given by transpose.
+
+See also `Matrix.transposeRingEquiv` for a version that doesn't take the opposite of `α`,
+given that its multiplication is commutative. -/
 @[simps apply symm_apply]
 def mopMatrix {α} [Mul α] [AddCommMonoid α] : 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
+  map_mul' _ _ := unop_injective <| by ext; simp [mul_apply]
+  map_add' _ _ := rfl
 
 end RingEquiv
 
@@ -721,8 +720,10 @@ theorem mapMatrix_trans (f : α ≃ₐ[R] β) (g : β ≃ₐ[R] γ) :
   rfl
 
 /-- 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`. -/
+`Matₙₓₙ(αᵒᵖ) ≅ (Matₙₓₙ(R))ᵒᵖ` given by transpose.
+
+See also `Matrix.transposeAlgEquiv` for a version that doesn't take the opposite of `α`,
+given that its multiplication is commutative. -/
 @[simps!] def mopMatrix : Matrix m m αᵐᵒᵖ ≃ₐ[R] (Matrix m m α)ᵐᵒᵖ where
   __ := RingEquiv.mopMatrix
   commutes' _ := MulOpposite.unop_injective <| by
@@ -894,7 +895,10 @@ theorem transposeLinearEquiv_symm [Semiring R] [AddCommMonoid α] [Module R α]
 variable {m n R α}
 variable (m α)
 
-/-- `Matrix.transpose` as a `RingEquiv` to the opposite ring -/
+/-- `Matrix.transpose` as a `RingEquiv` to the opposite ring.
+
+See also `RingEquiv.mopMatrix` for a version that doesn't require `α` to have commutative
+multiplication, by taking its opposite. -/
 @[simps!]
 def transposeRingEquiv [AddCommMonoid α] [CommMagma α] [Fintype m] :
     Matrix m m α ≃+* (Matrix m m α)ᵐᵒᵖ where
@@ -914,7 +918,10 @@ theorem transpose_list_prod [CommSemiring α] [Fintype m] [DecidableEq m] (l : L
 
 variable (R m α)
 
-/-- `Matrix.transpose` as an `AlgEquiv` to the opposite ring -/
+/-- `Matrix.transpose` as an `AlgEquiv` to the opposite ring.
+
+See also `AlgEquiv.mopMatrix` for a version that doesn't require `α` to have commutative
+multiplication, by taking its opposite. -/
 @[simps!]
 def transposeAlgEquiv [CommSemiring R] [CommSemiring α] [Fintype m] [DecidableEq m] [Algebra R α] :
     Matrix m m α ≃ₐ[R] (Matrix m m α)ᵐᵒᵖ where

Mathlib/LinearAlgebra/Matrix/Defs.lean

@@ -135,7 +135,16 @@ theorem map_injective {f : α → β} (hf : Function.Injective f) :
 theorem map_involutive {f : α → α} (hf : Function.Involutive f) :
     Function.Involutive fun M : Matrix m n α ↦ M.map f := by intro; simp [hf]
 
-/-- The transpose of a matrix. -/
+/-- The transpose of a matrix.
+
+This is available in bundled forms as:
+* `Matrix.transposeAddEquiv`
+* `Matrix.transposeLinearEquiv`
+* `Matrix.transposeRingEquiv`
+* `Matrix.transposeAlgEquiv`
+* `RingEquiv.mopMatrix`
+* `AlgEquiv.mopMatrix`
+-/
 def transpose (M : Matrix m n α) : Matrix n m α :=
   of fun x y => M y x