English
There exists a unit u and exponent n such that discr K (hζ.powerBasis K).basis = u * p^n in the IsCyclotomicExtension setting.
Русский
Существует единица u и показатель n так, что дискриминант равен u * p^n.
LaTeX
$$$\\exists u∈ℤ^{×},\\exists n∈ℕ,\\; \\mathrm{discr}_K( h\\zeta.powerBasis K).basis = u \\cdot p^{n}$$$
Lean4
/-- If `p` is a prime and `IsCyclotomicExtension {p ^ k} K L`, then there are `u : ℤˣ` and
`n : ℕ` such that the discriminant of `hζ.powerBasis K` is `u * p ^ n`. Often this is enough and
less cumbersome to use than `IsCyclotomicExtension.discr_prime_pow`. -/
theorem discr_prime_pow_eq_unit_mul_pow [IsCyclotomicExtension {p ^ k} K L] [hp : Fact p.Prime]
(hζ : IsPrimitiveRoot ζ (p ^ k)) (hirr : Irreducible (cyclotomic (p ^ k) K)) :
∃ (u : ℤˣ) (n : ℕ), discr K (hζ.powerBasis K).basis = u * p ^ n :=
by
rw [discr_prime_pow hζ hirr]
by_cases heven : Even ((p ^ k).totient / 2)
· exact ⟨1, p ^ (k - 1) * ((p - 1) * k - 1), by rw [heven.neg_one_pow]; simp⟩
· exact ⟨-1, p ^ (k - 1) * ((p - 1) * k - 1), by rw [(not_even_iff_odd.1 heven).neg_one_pow]; simp⟩
