Zulip Chat Archive
Stream: general
Topic: coe_inv
Yaël Dillies (May 29 2022 at 10:57):
Why is docs#coe_inv in the root namespace, @Patrick Massot?
Floris van Doorn (May 29 2022 at 11:00):
I think it would be nice to put a whole sequence of lemmas in that file in the namespace uniform_space.completion. Feel free to resurrect branch#coe_inv (or start from scratch).
Patrick Massot (May 29 2022 at 11:54):
There is no good reason at all, this is a historical accident.
Yaël Dillies (May 31 2022 at 20:55):
Last updated: Dec 20 2023 at 11:08 UTC