∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {ι : Type u_3}
  [inst_3 : Fintype ι] {f : ι → R} {x : ι → M}, Module.IsTrivialRelation f x → ∑ i, f i • x i = 0