# Zulip Chat Archive

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