Zulip Chat Archive

Stream: maths

Topic: localisation


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

view this post on Zulip Johan Commelin (Nov 23 2018 at 20:33):

Or something similar to that?

view this post on Zulip Kenny Lau (Nov 23 2018 at 20:34):

yes...

view this post on Zulip Johan Commelin (Nov 23 2018 at 20:34):

I don't think that is in mathlib.

view this post on Zulip Kenny Lau (Nov 23 2018 at 20:34):

it's in limbo...

view this post on Zulip Johan Commelin (Nov 23 2018 at 20:34):

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

view this post on Zulip Kenny Lau (Nov 23 2018 at 20:35):

https://github.com/leanprover/mathlib/pull/481/files#diff-8b1b305bf224a13c5239cddad4405491R131

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

view this post on Zulip Johan Commelin (Nov 23 2018 at 20:39):

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

view this post on Zulip Kevin Buzzard (Nov 23 2018 at 20:39):

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

view this post on Zulip Kevin Buzzard (Nov 23 2018 at 20:39):

So now I just don't read them.

view this post on Zulip Johan Commelin (Nov 23 2018 at 20:43):

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

view this post on Zulip Johan Commelin (Nov 23 2018 at 20:44):

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

view this post on Zulip Kenny Lau (Nov 23 2018 at 20:44):

...right

view this post on Zulip Patrick Massot (Nov 23 2018 at 20:54):

:open_mouth: I also missed that PR!

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