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

Last updated: May 08 2021 at 05:14 UTC