∀ {ι : Type u_1} {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Finite ι] [inst_4 : DecidableEq ι] (b : Module.Basis ι R M) (i j : ι),
  b.equivFun (b i) j = if i = j then 1 else 0