feat(LinearAlgebra/Matrix/Defs): lift more algebraic classes

Author: SnirBroshi

Mathlib/Algebra/Group/Pi/Basic.lean

@@ -43,13 +43,21 @@ variable (x y : ∀ i, f i) (i : I)
 
 namespace Pi
 
+@[to_additive]
+instance isMulCommutative [∀ i, Mul (f i)] [∀ i, IsMulCommutative (f i)] :
+    IsMulCommutative (∀ i, f i) where
+  is_comm.comm _ _ := by ext; apply mul_comm'
+
+@[to_additive]
+instance commMagma [∀ i, CommMagma (f i)] : CommMagma (∀ i, f i) where
+  mul_comm _ _ := by ext; apply mul_comm
+
 @[to_additive]
 instance semigroup [∀ i, Semigroup (f i)] : Semigroup (∀ i, f i) where
   mul_assoc := by intros; ext; exact mul_assoc _ _ _
 
 @[to_additive]
 instance commSemigroup [∀ i, CommSemigroup (f i)] : CommSemigroup (∀ i, f i) where
-  mul_comm := by intros; ext; exact mul_comm _ _
 
 @[to_additive]
 instance mulOneClass [∀ i, MulOneClass (f i)] : MulOneClass (∀ i, f i) where
@@ -69,8 +77,7 @@ instance monoid [∀ i, Monoid (f i)] : Monoid (∀ i, f i) where
   npow_succ := by intros; ext; exact Monoid.npow_succ _ _
 
 @[to_additive]
-instance commMonoid [∀ i, CommMonoid (f i)] : CommMonoid (∀ i, f i) :=
-  { monoid, commSemigroup with }
+instance commMonoid [∀ i, CommMonoid (f i)] : CommMonoid (∀ i, f i) where
 
 @[to_additive Pi.subNegMonoid]
 instance divInvMonoid [∀ i, DivInvMonoid (f i)] : DivInvMonoid (∀ i, f i) where

Mathlib/LinearAlgebra/Matrix/Defs.lean

@@ -220,6 +220,39 @@ instance distribMulAction [Monoid R] [AddMonoid α] [DistribMulAction R α] :
 instance module [Semiring R] [AddCommMonoid α] [Module R α] : Module R (Matrix m n α) :=
   inferInstanceAs <| Module R (m → n → α)
 
+instance [Add α] [IsAddCommutative α] : IsAddCommutative <| Matrix m n α :=
+  inferInstanceAs <| IsAddCommutative <| m → n → α
+
+instance [AddCommMagma α] : AddCommMagma <| Matrix m n α :=
+  inferInstanceAs <| AddCommMagma <| m → n → α
+
+instance [Add α] [IsLeftCancelAdd α] : IsLeftCancelAdd <| Matrix m n α :=
+  inferInstanceAs <| IsLeftCancelAdd <| m → n → α
+
+instance [Add α] [IsRightCancelAdd α] : IsRightCancelAdd <| Matrix m n α :=
+  inferInstanceAs <| IsRightCancelAdd <| m → n → α
+
+instance [Add α] [IsCancelAdd α] : IsCancelAdd <| Matrix m n α :=
+  inferInstanceAs <| IsCancelAdd <| m → n → α
+
+instance [AddLeftCancelSemigroup α] : AddLeftCancelSemigroup <| Matrix m n α :=
+  inferInstanceAs <| AddLeftCancelSemigroup <| m → n → α
+
+instance [AddRightCancelSemigroup α] : AddRightCancelSemigroup <| Matrix m n α :=
+  inferInstanceAs <| AddRightCancelSemigroup <| m → n → α
+
+instance [AddLeftCancelMonoid α] : AddLeftCancelMonoid <| Matrix m n α :=
+  inferInstanceAs <| AddLeftCancelMonoid <| m → n → α
+
+instance [AddRightCancelMonoid α] : AddRightCancelMonoid <| Matrix m n α :=
+  inferInstanceAs <| AddRightCancelMonoid <| m → n → α
+
+instance [AddCancelMonoid α] : AddCancelMonoid <| Matrix m n α :=
+  inferInstanceAs <| AddCancelMonoid <| m → n → α
+
+instance [AddCancelCommMonoid α] : AddCancelCommMonoid <| Matrix m n α :=
+  inferInstanceAs <| AddCancelCommMonoid <| m → n → α
+
 section
 
 @[simp]