Zulip Chat Archive

Stream: new members

Topic: R^n


view this post on Zulip 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:

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip 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)"

view this post on Zulip 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}?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Anatole Dedecker (Aug 13 2020 at 09:55):

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

view this post on Zulip Anatole Dedecker (Aug 13 2020 at 09:56):

But yeah I told him about hidden isomorphisms and all

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 12:13):

So this shows that your definition is a better implementation

view this post on Zulip Adam Topaz (Aug 13 2020 at 13:55):

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


Last updated: May 08 2021 at 05:14 UTC