feat(complex/roots_of_unity):  extensionality (#13431)
feat(complex/roots_of_unity):  extensionality (#13431)

Primitive roots are equal iff their arguments are equal. Adds some useful specialisations, too.





leanprover-community/mathlib,leanprover-community/mathlib