# Zulip Chat Archive

## Stream: new members

### Topic: linear independent

#### Alena Gusakov (Apr 04 2023 at 17:17):

Hi all,

This might be a little bit of a dumb question but I'm trying to understand the design of linear_independent and how to use it. I'm trying to use some of the existing lemmas for matroid proofs, but I keep tripping up on the two different ways that a set of vectors can be expressed and I'm not really sure which to use, how to go between them, etc. More specifically, I'm trying to talk about the image of a function $\phi : E \rightarrow (ι → 𝔽)$ that maps into a set of vectors, and we have

```
linear_independent 𝔽 (coe : (φ '' X) → (ι → 𝔽))
```

but also we can express it like

```
linear_independent 𝔽 (λ (e : X), φ (e : E))
```

For example, I want to use

```
lemma finrank_span_set_eq_card (s : set V) [fintype s]
(hs : linear_independent K (coe : s → V)) :
finrank K (span K s) = s.to_finset.card
```

which clearly uses the `coe`

expression.

#### Johan Commelin (Apr 04 2023 at 17:25):

@Alena Gusakov can you say a bit more about what `X`

is?

#### Alena Gusakov (Apr 04 2023 at 17:26):

Johan Commelin said:

Alena Gusakov can you say a bit more about what

`X`

is?

Sure! `X`

is just an arbitrary `set E`

, where `E`

is just a type for now (in our case it's the ground set of the matroid but I don't think that is necessary to know)

#### Johan Commelin (Apr 04 2023 at 17:27):

Is it important that `X`

is a `set E`

? Or is it useful to think about `X`

as an "indexed family of elements of `E`

"?

#### Alena Gusakov (Apr 04 2023 at 17:29):

I suppose you could view it as an indexed family of elements, but in the definition I have it as a set currently, I can provide an MWE if that helps!

#### Johan Commelin (Apr 04 2023 at 17:30):

If you can explain in a words a bit of the background that might also help. What is the intuitive meaning/role of `X`

?

#### Johan Commelin (Apr 04 2023 at 17:31):

Is it supposed to be a basis? Or a random set? Where does it come from? How is it used?

#### Yaël Dillies (Apr 04 2023 at 17:33):

I think docs#linear_independent.image_of_comp is one direction.

#### Alena Gusakov (Apr 04 2023 at 17:33):

Johan Commelin said:

Is it supposed to be a basis? Or a random set? Where does it come from? How is it used?

So `X`

is an arbitrary set of elements in a representable matroid, through which I'm trying to write some helper lemmas about the relationship between independence of a set in a matroid and linear independence of its representation. I.e. if a set `X`

is independent in `matroid E`

, then when you take its representation over some field $\mathbb{F}$ (which will be a set of vectors in some vector space over $\mathbb{F}$) you get a linearly independent set, and if it's not independent then the representation will not be linearly independent.

#### Yaël Dillies (Apr 09 2023 at 10:23):

For future reference, the lemma Alena was looking for is docs#linear_independent_image

Last updated: Dec 20 2023 at 11:08 UTC