English
For IsCyclotomicExtension {p^k} over ℚ and ζ primitive, the discriminant of the basis subOnePowerBasis is given by a closed form involving totient and p-powers.
Русский
Для IsCyclotomicExtension {p^k} над ℚ и ζ примитивного, дискриминант базиса subOnePowerBasis задаётся явной формулой через тау-функцию и p-степени.
LaTeX
$$$\operatorname{discr} \mathbb{Q}(\text{ζ}-1) = (-1)^{((p^k).totient)/2} \cdot p^{p^{k-1}((p-1)\,k-1)}$$$
Lean4
/-- The discriminant of the power basis given by `ζ - 1`. -/
theorem discr_prime_pow_ne_two' [IsCyclotomicExtension {p ^ (k + 1)} ℚ K] (hζ : IsPrimitiveRoot ζ (p ^ (k + 1)))
(hk : p ^ (k + 1) ≠ 2) :
discr ℚ (hζ.subOnePowerBasis ℚ).basis =
(-1) ^ ((p ^ (k + 1)).totient / 2) * p ^ (p ^ k * ((p - 1) * (k + 1) - 1)) :=
by
rw [← discr_prime_pow_ne_two hζ (cyclotomic.irreducible_rat (NeZero.pos _)) hk]
exact hζ.discr_zeta_eq_discr_zeta_sub_one.symm
