{R : Type u_1} →
  {M : Type u_2} →
    {ι : Type u_5} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] →
            [Fintype ι] → [DecidableEq ι] → Module.Basis ι R M → Module.Basis (ι × ι) R (Module.End R M)