Commit 2025-11-25 11:53 24d282ff

feat(CyclotomicFields): general formula for the discriminant (#29997) Add the general formula for the discriminant of a cyclotomic field:

theorem IsCyclotomicExtension.Rat.discr (n : ℕ) [hn : NeZero n] [hK : IsCyclotomicExtension {n} ℚ K] :
    discr K = (-1) ^ (φ n / 2) * (n ^ n.totient / ∏ p ∈ n.primeFactors, p ^ (n.totient / (p - 1)))

Also rename existing theorems from absdiscr_* to discr_*