∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] {V : Type u_1}
  [inst_3 : AddCommGroup V] [inst_4 : Module R V] (b : Module.Basis n R V) (M : GL n R) (v : V),
  ((Matrix.GeneralLinearGroup.toLin' b) M).toLinearEquiv v = (Fintype.linearCombination R ⇑b) ((↑M).mulVec ⇑(b.repr v))