Zulip Chat Archive

Stream: maths

Topic: lost algebraic facts

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)

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

Kevin Buzzard (Mar 03 2019 at 17:08):

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

Kevin Buzzard (Mar 03 2019 at 17:12):

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

Kevin Buzzard (Mar 03 2019 at 17:13):

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

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: Dec 20 2023 at 11:08 UTC