English
Let p be an odd prime and K ⊆ L be fields with an IsCyclotomicExtension of {p} over K. If the p-th cyclotomic polynomial over K is irreducible, then the discriminant of K with respect to the power basis generated by a primitive p-th root equals (-1)^{(p−1)/2} p^{p−2}. In particular, Disc_K(basis) = (-1)^{(p−1)/2} p^{p−2}.
Русский
Пусть p — нечётное простое число, и рассматриваются поля K ⊆ L с циклотомическим расширением {p} над K. Если цирколомическая сумма p-й степени над K irreducible, то дискриминант дискриминантного расширения относительно базиса мощности, порождённого примитивным p-й корнем корней единств, равен (-1)^{(p−1)/2} p^{p−2}. В частности, дискриминант циклотомического поля ℚ(ζ_p) равен -p^{p−2} при p=3.
LaTeX
$$$\operatorname{discr} \, K\bigl( (h\zeta. powerBasis\, K).basis \bigr) = (-1)^{\frac{p-1}{2}} \cdot p^{p-2}$$$
Lean4
/-- If `p` is an odd prime and `IsCyclotomicExtension {p} K L`, then
`discr K (hζ.powerBasis K).basis = (-1) ^ ((p - 1) / 2) * p ^ (p - 2)` if
`Irreducible (cyclotomic p K)`. -/
theorem discr_odd_prime [IsCyclotomicExtension { p } K L] [hp : Fact p.Prime] (hζ : IsPrimitiveRoot ζ p)
(hirr : Irreducible (cyclotomic p K)) (hodd : p ≠ 2) :
discr K (hζ.powerBasis K).basis = (-1) ^ ((p - 1) / 2) * p ^ (p - 2) :=
by
have : IsCyclotomicExtension {p ^ (0 + 1)} K L :=
by
rw [zero_add, pow_one]
infer_instance
have hζ' : IsPrimitiveRoot ζ (p ^ (0 + 1)) := by simpa using hζ
convert discr_prime_pow_ne_two hζ' (by simpa [hirr]) (by simp [hodd]) using 2
· rw [zero_add, pow_one, totient_prime hp.out]
· rw [_root_.pow_zero, one_mul, zero_add, mul_one, Nat.sub_sub]
