Zulip Chat Archive
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?
Kenny Lau (Nov 23 2018 at 20:34):
yes...
Johan Commelin (Nov 23 2018 at 20:34):
I don't think that is in mathlib.
Kenny Lau (Nov 23 2018 at 20:34):
it's in limbo...
Johan Commelin (Nov 23 2018 at 20:34):
/me searches for https://github.com/kckennylau/limbo
Kenny Lau (Nov 23 2018 at 20:35):
https://github.com/leanprover/mathlib/pull/481/files#diff-8b1b305bf224a13c5239cddad4405491R131
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
Kenny Lau (Nov 23 2018 at 20:44):
...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: Dec 20 2023 at 11:08 UTC