mathlib

7bc2e9ef - feat(ring_theory/polynomial/cyclotomic): add cyclotomic.irreducible (#5642)

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.