∀ (R : Type u_1) (M : Type u_2) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Module.Free R M]
  {m : Type u_3} {n : Type u_4} [Finite m] [Finite n], Module.Free R (Matrix m n M)