∀ {m : Type u_2} {n : Type u_3} {R : Type u_6} [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : NonAssocSemiring R]
  {A B : Matrix m n R}, A = B ↔ ∀ (x : Matrix n m R), (A * x).trace = (B * x).trace