Zulip Chat Archive

Stream: Is there code for X?

Topic: if f o g is linearly independent then so is g


view this post on Zulip Kenny Lau (Sep 01 2020 at 15:35):

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

view this post on Zulip Kenny Lau (Sep 01 2020 at 15:50):

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

Last updated: May 07 2021 at 18:19 UTC