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

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

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):

docs#is_basis.le_span

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

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)


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