The direct sumβ¨πβπΌππ of (right) modules(ππ)πβπΌ over π is their coproduct in π π¬ππ½. linalg
It may be constructed as tuples with componentwise addition.
Internal direct sum
π is the direct sumβ¨πβπΌππ iff every π£βπ may be written as the sum of finitely many π£πβππ in precisely one way.