mathlib

552a4709 - feat(number_theory/cyclotomic/rat): the ring of integers of cyclotomic fields. (#13585)

feat(number_theory/cyclotomic/rat): the ring of integers of cyclotomic fields. (#13585) We compute the ring of integers of a `p ^ n`-th cyclotomic extension of `ℚ`. From flt-regular Co-authored-by: Eric Rodriguez <ericrboidi@gmail.com>