∀ {A : Type u_3} [inst : Ring A] {ι : Type u_5} {relations : ι → Module.Relations A} {N : Type u_1}
  [inst_1 : AddCommGroup N] [inst_2 : Module A N] (s : (Module.Relations.directSum relations).Solution N) (i : ι)
  (r : (relations i).R), (Finsupp.linearCombination A fun g => s.var ⟨i, g⟩) ((relations i).relation r) = 0