mathlib

4a5728fe - chore(number_theory/cyclotomic/zeta): generalize to primitive roots (#11941)

chore(number_theory/cyclotomic/zeta): generalize to primitive roots (#11941) This was done as `(zeta p ℤ ℤ[ζₚ] : ℚ(ζₚ)) = zeta p ℚ ℚ(ζₚ)` is independent of Lean's type theory. Allows far more flexibility with results. Co-authored-by: Eric Rodriguez <37984851+ericrbg@users.noreply.github.com>