Commit 2021-01-07 13:09 7bc2e9ef
View on Github →feat(ring_theory/polynomial/cyclotomic): add cyclotomic.irreducible (#5642)
I proved irreducibility of cyclotomic polynomials, showing that cyclotomic n Z is the minimal polynomial of any primitive root of unity.