Finitely generated product (sub)modules

theorem Submodule.FG.prod {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {P : Type u_3} [AddCommMonoid P] [Module R P] {sb : Submodule R M} {sc : Submodule R P} (hsb : sb.FG) (hsc : sc.FG) : (sb.prod sc).FG

instance Module.Finite.prod {R : Type u_1} {M : Type u_2} {N : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [hM : Module.Finite R M] [hN : Module.Finite R N] : Module.Finite R (M × N)