Bases for direct sum of modules

This file defines a Module.Free instance for the direct sum of modules.

Implementation notes

Currently, to get a basis on ⨁ i, M i from a basis on each M i, use DFinsupp.basis (using that the types are defeq).

instance Module.Free.directSum (R : Type u_1) [Semiring R] {ι : Type u_2} (M : ι → Type u_3) [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [∀ (i : ι), Free R (M i)] : Free R (DirectSum ι fun (i : ι) => M i)