Zulip Chat Archive

Stream: general

Topic: linear_independent vs span


view this post on Zulip Scott Morrison (May 29 2020 at 12:34):

Am I allowed to be upset that linear_independent takes an indexed family, while span takes a set?

view this post on Zulip Scott Morrison (May 29 2020 at 12:35):

Is there a better way to state

lemma linear_independent.fin_succ (n : ) (ι : fin (n+1)  V)
  ( : linear_independent K (ι  fin.cast_succ))
  (hx : ι (fin.last n)  span K (set.range (ι  @fin.cast_succ n))) :
  linear_independent K ι :=

and does anyone have a proof that doesn't involved mucking about with sets too much? I would like this to be an easy consequence of the existing linear_independent.insert.

view this post on Zulip Scott Morrison (May 29 2020 at 12:36):

Or, to #xy this, if I'm planning on proving some vectors i : fin n \to V are linearly independent by inductively showing each initial segment of them are linearly independent, which lemmas am I meant to use to say this?

view this post on Zulip Johan Commelin (May 29 2020 at 12:53):

Scott Morrison said:

Am I allowed to be upset that linear_independent takes an indexed family, while span takes a set?

I think you are

view this post on Zulip Reid Barton (May 29 2020 at 12:53):

linear_independent has to be a family, while for span it doesn't matter so much.

view this post on Zulip Johan Commelin (May 29 2020 at 13:01):

linear_independent used to be a set, I think

view this post on Zulip Johan Commelin (May 29 2020 at 13:01):

Before the monster-refactor of linear algebra and finsupp, about a year ago


Last updated: May 08 2021 at 04:14 UTC