Topic: euclidean domains PR
Scott Morrison (Apr 04 2018 at 23:11):
I think https://github.com/leanprover/mathlib/pull/78 is at this point waiting either to be merged or for further comments.
Scott Morrison (Apr 04 2018 at 23:12):
I hope eventually it can be merged, so I can tick off the last box for Louis' summer project.
Mario Carneiro (Apr 05 2018 at 04:24):
I merged Louis' PR. There are some minor things that I notice, but it's best to just let that stuff evolve inside mathlib, it's gone through the ringer already and it came out nicely
Last updated: May 12 2021 at 23:13 UTC