Stream: maths

Topic: localisation

Johan Commelin (Nov 23 2018 at 20:33):

@Kenny Lau Did you have a proof somewhere that if you localise a ring at S, then S maps to units of the localisation?

Johan Commelin (Nov 23 2018 at 20:33):

Or something similar to that?

yes...

Johan Commelin (Nov 23 2018 at 20:34):

I don't think that is in mathlib.

it's in limbo...

Johan Commelin (Nov 23 2018 at 20:34):

/me searches for https://github.com/kckennylau/limbo

Kevin Buzzard (Nov 23 2018 at 20:37):

it's in limbo...

Just to comment that the @kbuzzard in that PR had no visible effect (in the sense that I didn't notice anything). I've only just seen this PR now.

Johan Commelin (Nov 23 2018 at 20:39):

Shouldn't that give you something in your GitHub notification area (or send you an email)?

Kevin Buzzard (Nov 23 2018 at 20:39):

Yeah but now I switched GH notifications on I always have 100 notifications.

Kevin Buzzard (Nov 23 2018 at 20:39):

So now I just don't read them.

Johan Commelin (Nov 23 2018 at 20:43):

Hmmm, maybe you should be more careful in which repositories you watch...

Johan Commelin (Nov 23 2018 at 20:44):

Anyway, @Kenny Lau it's cool that this is coming to mathlib in some near future

...right

Patrick Massot (Nov 23 2018 at 20:54):

:open_mouth: I also missed that PR!

Patrick Massot (Nov 23 2018 at 20:54):

I vote for reviewing that PR! And also the #where PR

Last updated: May 12 2021 at 08:14 UTC