# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: linear dependence of more than dimension

#### Bhavik Mehta (Jun 03 2020 at 16:58):

If I have k vectors in a vector space with dimension <k, they're linearly dependent - what's the closest thing in mathlib to this?

#### Johan Commelin (Jun 03 2020 at 16:59):

What kind of statement would you like?

#### Johan Commelin (Jun 03 2020 at 17:00):

Some sort of `lc`

that is nonzero, but whose sum evaluates to `0`

, via `lc.total`

?

#### Johan Commelin (Jun 03 2020 at 17:00):

I haven't touched this part of the library since the refactor last year... so maybe everything is different now.

#### Johan Commelin (Jun 03 2020 at 17:01):

I think `lc`

is maybe gone, but there is now `finsupp.total`

?

#### Bhavik Mehta (Jun 03 2020 at 17:01):

I'd be happy with that, `¬ linear_independent R v`

would be fine too

#### Johan Commelin (Jun 03 2020 at 17:13):

I think this would work https://leanprover-community.github.io/mathlib_docs/linear_algebra/finsupp.html#finsupp.total

#### Bhavik Mehta (Jun 03 2020 at 17:15):

I don't see how to relate this to the dimension though

#### Johan Commelin (Jun 03 2020 at 17:15):

https://leanprover-community.github.io/mathlib_docs/linear_algebra/basis.html#exists_subset_is_basis

#### Johan Commelin (Jun 03 2020 at 17:15):

If your family is lin.indep, use :up: to extend it to a basis

#### Johan Commelin (Jun 03 2020 at 17:16):

After that, use the def of dimension to get a contradiction

#### Bhavik Mehta (Jun 03 2020 at 17:16):

Ah I see, thanks

#### Johan Commelin (Jun 03 2020 at 17:16):

Are you using `[finite_dimensional K V]`

?

#### Johan Commelin (Jun 03 2020 at 17:17):

Or do you want to prove it using cardinals and infinite dimensional spaces?

#### Chris Hughes (Jun 03 2020 at 17:17):

`is_basis.le_span`

looks okay.

#### Bhavik Mehta (Jun 03 2020 at 17:18):

I'm in a finite dimensional space

#### Johan Commelin (Jun 03 2020 at 17:18):

#### Bhavik Mehta (Jun 03 2020 at 17:20):

That looks harder than using the definition of dimension I think... (to me at least, before trying)

#### Chris Hughes (Jun 03 2020 at 17:25):

But there's actually a non trivial theorem here right? You need the fact that two bases have the same cardinality.

#### Bhavik Mehta (Jun 03 2020 at 17:26):

I don't think so, my new basis that Johan suggests to construct is bigger than the dimension, which contradicts the definition of dimension directly

#### Chris Hughes (Jun 03 2020 at 17:28):

The dimension is the cardinality of the smallest basis, so having one bigger isn't obviously a contradiction.

#### Reid Barton (Jun 03 2020 at 17:29):

I would be inclined to use `dim_le_injective`

plus something

#### Chris Hughes (Jun 03 2020 at 17:30):

I think it probably needs to be made into a lemma

#### Reid Barton (Jun 03 2020 at 17:30):

`linear_independent`

is already basically saying that the associated linear map is injective

#### Reid Barton (Jun 03 2020 at 17:30):

but maybe the API isn't quite in place for this

#### Reid Barton (Jun 03 2020 at 17:32):

Anyways yeah, there should be a lemma like `dim_span`

with an inequality in the conclusion

#### Reid Barton (Jun 03 2020 at 17:32):

What's with `dim_span`

anyways? Shouldn't it be a statement about `cardinal.mk ι`

?

#### Reid Barton (Jun 03 2020 at 17:33):

I know they're the same, but if we went to the effort to use a family then it seems like we should talk about the cardinality of the family (i.e. the indexing set) and not the image of the family, right?

#### Johan Commelin (Jun 03 2020 at 17:34):

I think the refactor into families was pretty painful

#### Johan Commelin (Jun 03 2020 at 17:34):

So in some places they might have chosen to avoid extra refactor

#### Johan Commelin (Jun 03 2020 at 17:35):

What we need is `linear_independent.le_dim`

#### Johan Commelin (Jun 03 2020 at 17:35):

Where is `dim_span`

?

#### Reid Barton (Jun 03 2020 at 17:35):

https://leanprover-community.github.io/mathlib_docs/linear_algebra/dimension.html#dim_span

#### Johan Commelin (Jun 03 2020 at 17:36):

Thanks!

#### Reid Barton (Jun 03 2020 at 17:42):

`dim_finsupp`

(or better, `dim_free`

once we have that language) also looks like a missing lemma

#### Reid Barton (Jun 03 2020 at 17:43):

oh maybe it's hiding elsewhere

#### Reid Barton (Jun 03 2020 at 17:44):

Interesting that `noncomputable`

doesn't show up in the docs

#### Johan Commelin (Jun 03 2020 at 17:58):

Reid Barton said:

Interesting that

`noncomputable`

doesn't show up in the docs

@Rob Lewis :up:

We could typeset all the declarations that don't have the `noncomputable`

tag in some faded gray... [/jk]

#### Gabriel Ebner (Jun 03 2020 at 18:06):

I vote for yellow-black danger stripes, these are surprisingly easy to do in CSS:

noncomputable_bg.png

#### Reid Barton (Jun 03 2020 at 18:07):

Upon reflection it's not quite `noncomputable`

that I care about, but rather "naked `choice`

"

#### Reid Barton (Jun 03 2020 at 18:07):

or arguably other bad things like equality at `Type`

, though that's even harder to detect

#### Reid Barton (Jun 03 2020 at 18:07):

https://leanprover-community.github.io/mathlib_docs/linear_algebra/finsupp_vector_space.html#equiv_of_dim_eq_dim was the declaration that jumped out at me as odd

#### Yakov Pechersky (Sep 02 2020 at 19:54):

Similar to Bhavik's question, what's the proper way to state $v_i \in \mathbb{R}^d, i = 1, \ldots, N, v_i$ linearly dependent?

#### Yakov Pechersky (Sep 02 2020 at 19:59):

```
import data.matrix.basic
import linear_algebra.basis
import linear_algebra.finite_dimensional
import data.real.basic
variables (N d : ℕ)
local notation `V` := (fin d → ℝ)
variables (v : fin N → V)
variables (lin_dep : ¬ linear_independent ℝ v)
```

#### Yakov Pechersky (Sep 02 2020 at 19:59):

Like so?

#### Anne Baanen (Sep 03 2020 at 10:19):

That seems to be the canonical way, also used in docs#linear_dependent_iff

Last updated: May 07 2021 at 21:10 UTC