## 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)

#### 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: May 19 2021 at 02:10 UTC