mathlib
fb9c5d30 - feat(cyclotomic/basic): diverse roots of unity lemmas (#11473)

Commit

4 years ago

feat(cyclotomic/basic): diverse roots of unity lemmas (#11473) From flt-regular.

Author

ericrbg

ericrbg

Parents

Loading