A finite direct sum of finite modules is finite

This file defines a Module.Finite instance for a finite direct sum of finite modules.

instance Module.Finite.instDFinsupp {R : Type u_1} {ι : Type u_2} [Semiring R] [Finite ι] (M : ι → Type u_3) [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [∀ (i : ι), Module.Finite R (M i)] : Module.Finite R (Π₀ (i : ι), M i)

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