English
For cyclotomic extension with p-th power n and primitive root ζ, the discriminant of the power basis given by ζ − 1 equals a closed formula involving p and totient(p^k).
Русский
Для циклотомического расширения с порядком p^k и примитивным ζ дискриминант базы ζ − 1 задаётся явной формулой в зависимости от p и φ(p^k).
LaTeX
$$$\operatorname{discr} \mathbb{Q}(\text{power basis of }(\zeta-1)) = (-1)^{\frac{φ(p^k)}{2}} \cdot p^{p^{k-1}((p-1)k-1)}$$$
Lean4
/-- If `Irreducible (cyclotomic p K)` (in particular for `K = ℚ`) and `p` is an odd prime,
then the norm of `ζ - 1` is `p`. -/
theorem norm_sub_one_of_prime_ne_two' [hpri : Fact p.Prime] [hcyc : IsCyclotomicExtension { p } K L]
(hζ : IsPrimitiveRoot ζ p) (hirr : Irreducible (cyclotomic p K)) (h : p ≠ 2) : norm K (ζ - 1) = p :=
by
replace hirr : Irreducible (cyclotomic (p ^ (0 + 1)) K) := by simp [hirr]
replace hζ : IsPrimitiveRoot ζ (p ^ (0 + 1)) := by simp [hζ]
haveI : IsCyclotomicExtension {p ^ (0 + 1)} K L := by simp [hcyc]
simpa using norm_sub_one_of_prime_ne_two hζ hirr h
