English
There exists u∈ℤˣ and n∈ℕ such that discr K (hζ.powerBasis K).basis = u * p^n, for IsCyclotomicExtension {p^k} K L.
Русский
Существуют u∈ℤˣ и n∈ℕ такие, что дискриминант равен u * p^n.
LaTeX
$$$\\exists u∈ℤ^{\\times},\\exists n∈ℕ,\\;\\mathrm{discr}_K( h\\zeta.powerBasis K).basis = u \\cdot p^{n}$$$
Lean4
/-- If `p` is a prime and `IsCyclotomicExtension {p ^ (k + 1)} K L`, then the discriminant of
`hζ.powerBasis K` is `(-1) ^ (p ^ k * (p - 1) / 2) * p ^ (p ^ k * ((p - 1) * (k + 1) - 1))`
if `Irreducible (cyclotomic (p ^ (k + 1)) K))`, and `p ^ (k + 1) ≠ 2`. -/
theorem discr_prime_pow_ne_two' [IsCyclotomicExtension {p ^ (k + 1)} K L] [hp : Fact p.Prime]
(hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) (hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)) (hk : p ^ (k + 1) ≠ 2) :
discr K (hζ.powerBasis K).basis = (-1) ^ (p ^ k * (p - 1) / 2) * p ^ (p ^ k * ((p - 1) * (k + 1) - 1)) := by
simpa [totient_prime_pow hp.out (succ_pos k)] using discr_prime_pow_ne_two hζ hirr hk
