∀ {R : Type u_1} {M : Type u_2} {ι : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Fintype ι] [inst_4 : DecidableEq ι] (b : Module.Basis ι R M) (a : M →ₗ[R] M),
  b.end.repr a = (Matrix.stdBasis R ι ι).repr ((LinearMap.toMatrix b b) a)