Experimenting with a "Sphere Eversion repo first, Mathlib second" policy --- it is satisfyingly faster to write code this way :-)
As I commented on Zulip "I have not really tried to combat some grossness in the proposed new file src/loops/smooth_barycentric.lean. I'm happy to polish this up too but I thought I'd request feedback first since we might be OK to leave the code there in a not-amazing-but-OK state and just move on to other things."
Experimenting with a "Sphere Eversion repo first, Mathlib second" policy --- it is satisfyingly faster to write code this way :-)
As I commented on Zulip "I have not really tried to combat some grossness in the proposed new file
src/loops/smooth_barycentric.lean. I'm happy to polish this up too but I thought I'd request feedback first since we might be OK to leave the code there in a not-amazing-but-OK state and just move on to other things."