David Kurniadi Angdinata

> So do you want both types of coordinates in Mathlib? What is the motivation for doing it that way, rather than just choosing one type of coordinates? I need...

Sure, give me a couple of hours and I'll hopefully update everything by today!

Thanks! I'll have a look later in the week. I don't mind merging this PR as a whole, but I don't want to set a precedent where 1000+ line feat...

@alreadydone do we actually need these? ``` lemma addZ_self {P : Fin 3 → R} : addZ P P = 0 lemma addX_self {P : Fin 3 → R} (hP...

This condenses the eight `natDegree/coeff_even/odd_preΨ'_even/odd` lemmas into one, but I think we still can't avoid the `natDegree/coeff_preΨ'_add_*` lemmas in the proof of `natDegree_coeff_preΨ'`? Maybe I'm missing something...

> @Multramate Have you tried to clean up the rest of my branch? If not, I'll try to see if I can golf the subsequent computations today. Thanks for waiting!...