# Zulip Chat Archive

## Stream: new members

### Topic: R^n

#### Anatole Dedecker (Aug 12 2020 at 23:38):

Ok so this is a dumb question as I am discovering mathlib's linear algebra library, but I can't find anything about ℝ^n being a vector_space :sweat_smile:

#### Jalex Stark (Aug 13 2020 at 01:59):

i actually don't know whether this answers your question, but have you watched anne baanen's video on linear algebra from lftcm2020?

#### Floris van Doorn (Aug 13 2020 at 02:24):

If you write `fin n -> ℝ`

(or even better `\i -> ℝ`

, possibly with `[fintype \i]`

) then `by apply_instance`

should find the instance docs#pi.semimodule . At least, I hope, since `vector_space`

is defined to be `semimodule`

.

#### Anatole Dedecker (Aug 13 2020 at 09:15):

Yes I thought about using `fin n -> \R`

, which definitely work, but I didn't know if it was the appropriate way to talk about R^n (I was expecting some kind of Cartesian product). Also thanks @Jalex Stark I'll watch this.

#### Anatole Dedecker (Aug 13 2020 at 09:21):

Fun fact, I told a friend of mine who didn't know Lean about defining R^n as `fin n -> \R`

(which I translated as `⟦1,n⟧ → ℝ`

), and I think he started to doubt my sanity

#### Kevin Buzzard (Aug 13 2020 at 09:28):

It doesn't matter what the implementation is to a user, and this implementation is easier to use than the inductive definition (which is the only other one I can imagine).

#### Anatole Dedecker (Aug 13 2020 at 09:30):

Indeed, but he just told me "that's not what R^n **is** (i.e a cartesian product)"

#### Kevin Buzzard (Aug 13 2020 at 09:46):

Then he needs to and learn about implementation v specification. Does he believe that 3 **is** {0,1,2}?

#### Kevin Buzzard (Aug 13 2020 at 09:47):

Because if he's using ZFC and he unwraps all the packaging, he might find out that this is what it **is**, except if he's looking at the real number 3, which of course **is** an uncountable set of Cauchy sequences.

#### Kevin Buzzard (Aug 13 2020 at 09:48):

A cartesian product only works for two sets. How can you use cartesian products for n sets?

#### Anatole Dedecker (Aug 13 2020 at 09:55):

He meant a recursive cartesian product, like $\mathbb{R}^n$ is $\mathbb{R}^{n-1} \times \mathbb{R}$

#### Anatole Dedecker (Aug 13 2020 at 09:56):

But yeah I told him about hidden isomorphisms and all

#### Kevin Buzzard (Aug 13 2020 at 12:13):

So he wants to prove e.g. that R^n is a group by induction on n? And in your definition you just get it immediately, right?

#### Kevin Buzzard (Aug 13 2020 at 12:13):

So this shows that your definition is a better implementation

#### Adam Topaz (Aug 13 2020 at 13:55):

I think the point in this case is that you need to think about $\mathbb{R}^S$ for some arbitrary set $S$, and $\mathbb{R}^n$ is the special case where $S$ is the canonical set of size n.

#### tsuki hao (Aug 08 2023 at 06:17):

May I ask how could R^n be defined in lean?

#### Moritz Doll (Aug 08 2023 at 06:42):

We have docs#EuclideanSpace but depending on the goal we prefer to state theorems in terms of arbitrary finite dimensional vector spaces.

#### tsuki hao (Aug 08 2023 at 07:04):

[Quoting…]

Thank you! I'll try it！

#### Flo (Florent Schaffhauser) (Aug 09 2023 at 08:26):

There is also the type `Vector ℝ n`

, whose terms are lists of real numbers, that have length `n`

. docs#Vector

#### Eric Wieser (Aug 09 2023 at 08:38):

It's very unlikely that you want that type

#### Flo (Florent Schaffhauser) (Aug 09 2023 at 10:15):

OK, so democratically I am wrong :-) But I cannot really see why it is *unlikely* that one might want that type.

Of course I do not know what the OP had in mind, whether they wanted `R^n`

with its canonical structure of Euclidean space, or just `n`

-tuples of real numbers. Would you agree in that case that this is the type to look at? Or would you recommend something like `Fin n → \R`

instead?.

But it sounded to me that the next question that may come to mind might be how to define `C^n`

then `Q^n`

, then `(Z/pZ)^n`

etc. So docs#EuclideanSpace might not be the ideal starting point.

I am just trying to understand why you think it is unlikely that the `Vector \R n`

type might be helpful :sweat_smile:

#### Eric Wieser (Aug 09 2023 at 10:21):

Flo (Florent Schaffhauser) said:

Of course I do not know what the OP had in mind, whether they wanted

`R^n`

with its canonical structure of Euclidean space, or just`n`

-tuples of real numbers. Would you agree in that case that this is the type to look at?

Even then, probably no. Chances are even if you don't want the metric space structure of docs#EuclideanSpace, you still want basic elementwise addition of tuples, which you do not get with docs#Vector.

Or would you recommend something like

`Fin n → \R`

instead?.

Yes, this is reasonable; you just have to avoid the trap that `norm ![3, 4] = 4`

not `5`

!

But it sounded to me that the next question that may come to mind might be how to define

`C^n`

then`Q^n`

, then`(Z/pZ)^n`

etc. So docs#EuclideanSpace might not be the ideal starting point.

docs#EuclideanSpace already works for $\mathbb{C}^n$. ~~Probably this is an argument that ~~ (Edit: it doesn't permit a real-vector-space structure, so you can't normalize vectors)`EuclideanSpace`

should be generalized to allow $\mathbb{Q}$ too...

#### Moritz Doll (Aug 09 2023 at 14:29):

`PiLp`

should work for `Fin n \to F`

as long as `F`

has a metric or a norm.

Last updated: Dec 20 2023 at 11:08 UTC