## Stream: general

### Topic: linear_independent vs span

#### 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?

#### 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)
(hι : 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.

#### 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?

#### 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

#### Reid Barton (May 29 2020 at 12:53):

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

#### Johan Commelin (May 29 2020 at 13:01):

linear_independent used to be a set, I think

#### 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