## Stream: maths

### Topic: Define linear function from matrix

#### Abhimanyu Pallavi Sudhir (Nov 14 2019 at 17:23):

How can I construct in Lean the linear transformation (as a function) given by an (infinite) set of vectors (in ℕ → ℝ), a proof that they are linearly independent, and their images?

On the subtype of ℕ → ℝ that is their span, of course.

#### Abhimanyu Pallavi Sudhir (Nov 14 2019 at 17:27):

I'm not very familiar with the linear_algebra in mathlib.

#### Abhimanyu Pallavi Sudhir (Nov 14 2019 at 17:28):

Oh I guess it's to_lin.

#### Abhimanyu Pallavi Sudhir (Nov 14 2019 at 17:29):

Or eval.

#### Kevin Buzzard (Nov 14 2019 at 17:31):

The linear transformation on what? Their span?

#### Kevin Buzzard (Nov 14 2019 at 17:31):

PS are you in the same room as me?

Yes.

And yes.

#### Abhimanyu Pallavi Sudhir (Nov 14 2019 at 17:41):

Apparently matrices don't work.

#### Abhimanyu Pallavi Sudhir (Nov 14 2019 at 17:42):

Because they're finite.

#### Abhimanyu Pallavi Sudhir (Nov 14 2019 at 17:43):

At least there must be a way to define a linear map from basis elements even if we were defining it on the entire space and not a subspace.

#### Mario Carneiro (Nov 14 2019 at 17:45):

The setup confuses me. What is the type of the input and output?

#### Abhimanyu Pallavi Sudhir (Nov 14 2019 at 17:48):

The type of the input is a submodule of ℕ → ℝ (given as the span of a set). The type of the output is ℝ as a module.

#### Mario Carneiro (Nov 14 2019 at 17:49):

is ℕ → ℝ the vector space or is it a countable family over ℝ?

#### Abhimanyu Pallavi Sudhir (Nov 14 2019 at 17:49):

It's the vector space.

#### Abhimanyu Pallavi Sudhir (Nov 14 2019 at 17:49):

But the map is defined only on a subtype of it.

#### Abhimanyu Pallavi Sudhir (Nov 14 2019 at 17:50):

The set of vectors is something like 1/(n+m) : m \in \nat

#### Mario Carneiro (Nov 14 2019 at 17:50):

what map? you only have a submodule

#### Abhimanyu Pallavi Sudhir (Nov 14 2019 at 17:50):

Right, but I can make it a subtype and it would still be a module.

#### Johan Commelin (Nov 14 2019 at 17:54):

@Abhimanyu Pallavi Sudhir If I understand you correctly, you don't really care about the vector space

#### Johan Commelin (Nov 14 2019 at 17:54):

So you have some family v : \iota → V of vectors

#### Johan Commelin (Nov 14 2019 at 17:54):

And you have a proof that they are linearly independent.

#### Johan Commelin (Nov 14 2019 at 17:54):

And you have a family f : \iota → W of "images"

#### Johan Commelin (Nov 14 2019 at 17:55):

And now you want the map from the span of the v i to W, that maps v i to f i.

Is that correct?

Yes.

#### Abhimanyu Pallavi Sudhir (Nov 14 2019 at 17:56):

Chris tells me linear_independent.repr is what I'm looking for.

#### Abhimanyu Pallavi Sudhir (Nov 14 2019 at 17:56):

I'm having a look at it.

#### Johan Commelin (Nov 14 2019 at 17:56):

I think that's right

Last updated: May 12 2021 at 08:14 UTC