mathlib3
1378eabf - feat(complex/roots_of_unity): extensionality (#13431)

Commit

4 years ago

feat(complex/roots_of_unity): extensionality (#13431) Primitive roots are equal iff their arguments are equal. Adds some useful specialisations, too.

Author

ericrbg

Parents