if f o g is linearly independent then so is g

Stream: Is there code for X?

[Kenny Lau]

If ⇑f ∘ g is linearly independent then g is also linearly independent

[Kenny Lau]

lemma linear_independent_of_comp {R : Type u} {M : Type v} {N : Type w} {ι : Type*}
  [comm_ring R] [add_comm_group M] [add_comm_group N] [module R M] [module R N]
  (f : M →ₗ[R] N) (v : ι → M) (hfv : linear_independent R (f ∘ v)) :
  linear_independent R v :=
linear_independent_iff'.2 $ λ s g hg i his,
have ∑ (i : ι) in s, g i • f (v i) = 0,
  by simp_rw [← f.map_smul, ← f.map_sum, hg, f.map_zero],
linear_independent_iff'.1 hfv s g this i his