# Zulip Chat Archive

## Stream: new members

### Topic: independent columns

#### Julian Berman (Dec 22 2020 at 04:18):

Is there something like `set`

which gives all families rather than sets? Context is:

```
import data.matrix.notation
import linear_algebra.linear_independent
def A : matrix _ _ ℚ := ![
![1, 0, 0, 1, 0, 0, 0],
![0, 1, 0, 1, 1, 1, 0],
![0, 0, 1, 0, 1, 1, 0]
]
def I := {x : set (fin 7) // linear_independent (fin 3 → ℚ) (λ i : x, A.transpose i)}
```

-- which I don't know is correct yet, I'm trying to say a type of "all collections of indices whose columns in A are linearly independent", but I see `linearly_independent`

is telling me to start with families rather than sets if I can, so is there a thing that given `fin 7`

will give me all of those maps directly, or am I doing that the way that's expected? (Including whether transposing is the way I'm supposed to pull off columns?)

#### Johan Commelin (Dec 22 2020 at 06:04):

@Julian Berman The code compiles, right?

I think you want to replace `(fin 3 → ℚ)`

with `ℚ`

, because you presumably want the columns to be linearly independent over the rationals. Otherwise, this seems like the way to go, to me.

#### Julian Berman (Dec 22 2020 at 06:24):

ah of course -- thanks. It does indeed compile, I just wasn't sure (besides whether it was idiomatic) if that was the right type (e.g. I couldn't yet prove that column 7 isn't in any set despite finding `linear_independent.ne_zero`

-- probably I'm close though, will give it another shot in the morning, thanks for the confirmation!.

#### Julian Berman (Dec 22 2020 at 14:43):

OK managed to get a little bit closer but I think my issue is struggling a bit to prove things about a subtype (or perhaps I'm confused about how to pull an element out of the set there)...

I'm not sure how to proceed from:

```
example : ∀ i : I, (6 : fin 7) ∉ i.val := begin
intro i,
have h := linear_independent.ne_zero i.property,
/-
2 goals
i : I,
h : (λ (i_1 : ↥(i.val)), A.transpose ↑i_1) ?m_1 ≠ 0
⊢ 6 ∉ i.val
i : I
⊢ ↥(i.val)
-/
end
```

I need to basically pass `6`

into `h`

right? Is that what `specialize`

is for?

#### Patrick Massot (Dec 22 2020 at 15:26):

The main source of trouble here is a bad implicit argument on docs#linear_independent.ne_zero.

#### Patrick Massot (Dec 22 2020 at 15:27):

You should start with:

```
import data.matrix.notation
import linear_algebra.linear_independent
def A : matrix _ _ ℚ := ![
![1, 0, 0, 1, 0, 0, 0],
![0, 1, 0, 1, 1, 1, 0],
![0, 0, 1, 0, 1, 1, 0]
]
def I := {x : set (fin 7) // linear_independent (fin 3 → ℚ) (λ i : x, A.transpose i)}
lemma linear_independent.ne_zero' {ι R M: Type*} {v : ι → M} [ring R] [add_comm_group M]
[module R M] [nontrivial R] (i : ι) (h : linear_independent R v) : v i ≠ 0 :=
h.ne_zero
example : ∀ i : I, (6 : fin 7) ∉ i.val := begin
intros i H,
apply i.property.ne_zero' (⟨6, H⟩ : i.val),
dsimp only,
end
```

And then open a PR fixing that broken binder.

#### Patrick Massot (Dec 22 2020 at 15:28):

The difference between `linear_independent.ne_zero'`

and `linear_independent.ne_zero`

is the `i`

argument is explicit.

#### Julian Berman (Dec 22 2020 at 15:38):

Aha... thank you! Will do.

Last updated: May 15 2021 at 00:39 UTC