English
Let p be a prime, k be a natural number, and K a field of characteristic zero with IsCyclotomicExtension {p^(k+1)} over Q. Then the absolute discriminant of K is given by Disc(K) = (-1)^{p^k(p-1)/2} · p^{p^k((p-1)(k+1) - 1)}.
Русский
Пусть p — простое число, k — натуральное число, K — тело характеристикой ноль, для которого выполняется IsCyclotomicExtension {p^(k+1)} over Q. Тогда абсолютный дискриминант поля K равен Disc(K) = (-1)^{p^k(p-1)/2} · p^{p^k((p-1)(k+1) - 1)}.
LaTeX
$$$\operatorname{Disc}(K) = (-1)^{\frac{p^k(p-1)}{2}} \cdot p^{\,p^k\big((p-1)(k+1) - 1\big)}$$$
Lean4
/-- We compute the absolute discriminant of a `p ^ (k + 1)`-th cyclotomic field.
Beware that in the case `p ^ k = 2` the formula uses `1 / 2 = 0`. See also the results below. -/
theorem absdiscr_prime_pow_succ [IsCyclotomicExtension {p ^ (k + 1)} ℚ K] :
haveI : NumberField K := IsCyclotomicExtension.numberField {p ^ (k + 1)} ℚ K
NumberField.discr K = (-1) ^ (p ^ k * (p - 1) / 2) * p ^ (p ^ k * ((p - 1) * (k + 1) - 1)) :=
by simpa [totient_prime_pow hp.out (succ_pos k)] using absdiscr_prime_pow p (k + 1) K
