mathlib
7fdeecc0 - chore(ring_theory/root_of_unity): move and split a file (#19144)

Commit
2 years ago
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`.
Parents
Loading