Commit 2022-02-10 23:42 4a5728fe
View on Github →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.