Proper way to define direct product of 2 modules

Stream: new members

[VayusElytra]

Hello, I saw in documentation that the traditional way to define the direct sum of a bunch of modules is to do something like:

open DirectSum

variable {R : Type u} [Semiring R]
variable {ι : Type v} [dec_ι : DecidableEq ι]
variable {M : ι → Type w} [∀ i, AddCommMonoid (M i)] [∀ i, Module R (M i)]

def Z := (⨁ i, M i)

This works fine if you have many modules to do a direct sum over, but what about if one just wants to do a direct sum of 2 modules? Is there a simpler way to do that?

[Kevin Buzzard]

import Mathlib.Algebra.Module.Prod

variable {R : Type*} [Semiring R]
variable {M N : Type*} [AddCommMonoid M] [AddCommMonoid N]
    [Module R M] [Module R N]

#synth Module R (M × N) -- works

[VayusElytra]

Thank you, that is indeed quite simple!