Commit 2023-06-02 16:27 7fdeecc0
View on Github →chore(ring_theory/root_of_unity): move and split a file (#19144)
We split ring_theory.roots_of_unity
(almost 1200 lines) into ring_theory.roots_of_unity.basic
and ring_theory.roots_of_unity.minpoly
. We also move analysis.complex.roots_of_unity
to ring_theory.roots_of_unity.complex
.