Zulip Chat Archive

Stream: Is there code for X?

Topic: Linear indep of nonzero smul


view this post on Zulip Adam Topaz (Feb 19 2021 at 17:31):

Do we have something like this?

import linear_algebra.linear_independent

variables (K V : Type*) [field K] [add_comm_group V] [vector_space K V]

lemma foo {ι : Type*} (f g : ι  V) (cond :  i,  a : K, a  0  a  f i = g i) :
  linear_independent K f  linear_independent K g := sorry

Last updated: May 07 2021 at 18:19 UTC