∀ {A : Type u} [inst : Ring A] {ι : Type w} [inst_1 : DecidableEq ι] {M : ι → Type v}
  [inst_2 : (i : ι) → AddCommGroup (M i)] [inst_3 : (i : ι) → Module A (M i)]
  (pres : (i : ι) → Module.Presentation A (M i)), (Module.Presentation.directSum pres).R = ((i : ι) × (pres i).R)