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