feat(Data/Matrix/Notation): relax Semiring to `NonUnitalNonAssocSem…

…iring` (#5092)

This came up in a real example. I was using Lean to make sure I had the right formulae for Strassen's algorithm. The following example was only able to succeed with (some of) these changes:
```lean
import Mathlib.Data.Matrix.Notation
import Mathlib.Tactic.NoncommRing

example (R : Type _) [NonUnitalNonAssocRing R]
  (a₁₁ a₁₂ a₂₁ a₂₂ b₁₁ b₁₂ b₂₁ b₂₂ : R) :
    let m₁ := (a₁₁ + a₂₂) * (b₁₁ + b₂₂)
    let m₂ := (a₂₁ + a₂₂) * b₁₁
    let m₃ := a₁₁ * (b₁₂ - b₂₂)
    let m₄ := a₂₂ * (b₂₁ - b₁₁)
    let m₅ := (a₁₁ + a₁₂) * b₂₂
    let m₆ := (a₂₁ - a₁₁) * (b₁₁ + b₁₂)
    let m₇ := (a₁₂ - a₂₂) * (b₂₁ + b₂₂)
    !![a₁₁, a₁₂;
       a₂₁, a₂₂] * !![b₁₁, b₁₂;
                      b₂₁, b₂₂] = !![m₁ + m₄ - m₅ + m₇, m₃ + m₅;
                                     m₂ + m₄,           m₁ - m₂ + m₃ + m₆] := by
  ext i j
  fin_cases i <;> fin_cases j <;> simp <;> noncomm_ring
```

Mathlib/Data/Matrix/Notation.lean

@@ -224,7 +224,7 @@ end Transpose
 
 section Mul
 
-variable [Semiring α]
+variable [NonUnitalNonAssocSemiring α]
 
 @[simp]
 theorem empty_mul [Fintype n'] (A : Matrix (Fin 0) n' α) (B : Matrix n' o' α) : A ⬝ B = of ![] :=
@@ -260,7 +260,7 @@ end Mul
 
 section VecMul
 
-variable [Semiring α]
+variable [NonUnitalNonAssocSemiring α]
 
 @[simp]
 theorem empty_vecMul (v : Fin 0 → α) (B : Matrix (Fin 0) o' α) : vecMul v B = 0 :=
@@ -295,7 +295,7 @@ end VecMul
 
 section MulVec
 
-variable [Semiring α]
+variable [NonUnitalNonAssocSemiring α]
 
 @[simp]
 theorem empty_mulVec [Fintype n'] (A : Matrix (Fin 0) n' α) (v : n' → α) : mulVec A v = ![] :=
@@ -325,7 +325,7 @@ end MulVec
 
 section VecMulVec
 
-variable [Semiring α]
+variable [NonUnitalNonAssocSemiring α]
 
 @[simp]
 theorem empty_vecMulVec (v : Fin 0 → α) (w : n' → α) : vecMulVec v w = ![] :=
@@ -355,7 +355,7 @@ end VecMulVec
 
 section Smul
 
-variable [Semiring α]
+variable [NonUnitalNonAssocSemiring α]
 
 -- @[simp] -- Porting note: simp can prove this
 theorem smul_mat_empty {m' : Type _} (x : α) (A : Fin 0 → m' → α) : x • A = ![] :=