Zulip Chat Archive

Stream: general

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