English
The direct sum has an obvious presentation obtained from the presentations of each M_i; i.e., the presentation of the direct sum is built from the family of presentations.
Русский
У прямой суммы есть очевидная презентация, получаемая из презентаций каждого M_i; презентация прямой суммы строится из семейства презентаций.
LaTeX
$$$\\text{Module.Presentation.directSum}(\\text{pres}) : \\text{Presentation } A(\\bigoplus_i M_i)$$$
Lean4
/-- The obvious presentation of the module `⨁ i, M i` that is obtained from
the data of presentations of the module `M i` for each `i`. -/
@[simps! G R relation]
noncomputable def directSum (pres : ∀ (i : ι), Presentation A (M i)) : Presentation A (⨁ i, M i) :=
ofIsPresentation (Relations.Solution.IsPresentation.directSum (fun i ↦ (pres i).toIsPresentation))
