Mathlib v3 is deprecated. Go to Mathlib v4

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.

Estimated changes