∀ {R : Type u_2} {M : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {x y : M} {S : Type u_6}
  [inst_3 : CommRing S] [IsDomain S] [inst_5 : Module S R] [inst_6 : Module S M] [SMulCommClass S R M]
  [IsScalarTower S R M] [Module.IsTorsionFree S R] (c : S),
  LinearIndependent R ![x, c • x + y] ↔ LinearIndependent R ![x, y]