Zulip Chat Archive

Stream: maths

Topic: lost algebraic facts


view this post on Zulip Patrick Massot (Mar 03 2019 at 16:59):

Still working on topology cleanup, I need someone to tell me whether https://github.com/leanprover-community/mathlib/blob/108486871aa0a7f0afd221c191766e9bebefde82/src/topology/algebra/quotient.lean#L115-L129 is already somewhere else. If not then I'd need to know where to put this (it has no reason to stay there)

view this post on Zulip Patrick Massot (Mar 03 2019 at 17:00):

same with https://github.com/leanprover-community/mathlib/blob/108486871aa0a7f0afd221c191766e9bebefde82/src/topology/algebra/quotient.lean#L139-L149

view this post on Zulip Kevin Buzzard (Mar 03 2019 at 17:08):

https://github.com/leanprover-community/mathlib/blob/108486871aa0a7f0afd221c191766e9bebefde82/src/group_theory/subgroup.lean#L283

view this post on Zulip Kevin Buzzard (Mar 03 2019 at 17:12):

https://github.com/leanprover-community/mathlib/blob/108486871aa0a7f0afd221c191766e9bebefde82/src/algebra/module.lean#L246

view this post on Zulip Kevin Buzzard (Mar 03 2019 at 17:13):

I knew those were there but I don't know about quotient_ring_saturate

view this post on Zulip Patrick Massot (Mar 03 2019 at 18:46):

Thanks Kevin! The second one is not what I needed, but the first one was clearly a duplicate


Last updated: May 19 2021 at 02:10 UTC