∀ {κ : Type w} (A : Type u) {B : Type v} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
  {κ' : Type u_7} (b : Module.Basis κ A B) (f : κ ≃ κ'),
  Algebra.traceMatrix A ⇑(b.reindex f) = (Matrix.reindex f f) (Algebra.traceMatrix A ⇑b)