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: Aug 03 2023 at 10:10 UTC