English
If IsCyclotomicExtension {p^k} ℚ K and ζ primitive, the discriminant of the zeta-based basis equals a product of a unit and p^n as in discr_prime_pow'.
Русский
Если IsCyclotomicExtension {p^k} над ℚ и ζ примитивен, дискриминант базиса ζ-based равен единице, умноженной на p^n.
LaTeX
$$$\exists u \in \mathbb{Z}^{\times}, \exists n \in \mathbb{N},\; \operatorname{discr} = u \cdot p^n$$$
Lean4
/-- The discriminant of the power basis given by `ζ - 1`. Beware that in the cases `p ^ k = 1` and
`p ^ k = 2` the formula uses `1 / 2 = 0` and `0 - 1 = 0`. It is useful only to have a uniform
result. See also `IsCyclotomicExtension.Rat.discr_prime_pow_eq_unit_mul_pow'`. -/
theorem discr_prime_pow' [IsCyclotomicExtension {p ^ k} ℚ K] (hζ : IsPrimitiveRoot ζ (p ^ k)) :
discr ℚ (hζ.subOnePowerBasis ℚ).basis = (-1) ^ ((p ^ k).totient / 2) * p ^ (p ^ (k - 1) * ((p - 1) * k - 1)) :=
by
rw [← discr_prime_pow hζ (cyclotomic.irreducible_rat (NeZero.pos _))]
exact hζ.discr_zeta_eq_discr_zeta_sub_one.symm
