{m : Type u_2} →
  {α : Type u_11} →
    {β : Type u_12} →
      [inst : Fintype m] →
        [DecidableEq m] →
          [inst_2 : NonAssocSemiring α] → [inst_3 : NonAssocSemiring β] → α ≃+* β → Matrix m m α ≃+* Matrix m m β