∀ (n : ℕ) (K : Type u) [inst : Field K] [inst_1 : CharZero K] [hn : NeZero n] [hK : IsCyclotomicExtension {n} ℚ K],
  (NumberField.discr K).natAbs = n ^ n.totient / ∏ p ∈ n.primeFactors, p ^ (n.totient / (p - 1))