!4#4677 RootsOfUnity.Basic

Stream: mathlib4

[Johan Commelin]

The top of this file is broken because of some silly coercion not working. If you know how to handle coes in Lean 4, please feel free to help out!

[Ruben Van de Velde]

The problem is that this file does a lot of coercion of the form (subtype of Rˣ) → Rˣ → R, which lean4 needs some hand-holding for

[Ruben Van de Velde]

20-ish errors left for anyone who'd like to pick it up

[Johan Commelin]

Wow, great job!