English
Let p be prime and K a field with IsCyclotomicExtension {p} over Q. Then the absolute discriminant of K satisfies Disc(K) = (-1)^{(p-1)/2} · p^{p-2}.
Русский
Пусть p — простое число и K тело с IsCyclotomicExtension {p} надQ. Тогда дискриминант поля K равен Disc(K) = (-1)^{(p-1)/2} · p^{p-2}.
LaTeX
$$$\operatorname{Disc}(K) = (-1)^{\frac{p-1}{2}} \cdot p^{p-2}$$$
Lean4
/-- We compute the absolute discriminant of a `p`-th cyclotomic field where `p` is prime. -/
theorem absdiscr_prime [IsCyclotomicExtension { p } ℚ K] :
haveI : NumberField K := IsCyclotomicExtension.numberField { p } ℚ K
NumberField.discr K = (-1) ^ ((p - 1) / 2) * p ^ (p - 2) :=
by
have : IsCyclotomicExtension {p ^ (0 + 1)} ℚ K :=
by
rw [zero_add, pow_one]
infer_instance
rw [absdiscr_prime_pow_succ p 0 K]
simp [Nat.sub_sub]
