English
There exists a unit u and exponent n such that the discriminant of the ζ − 1 power basis equals u · p^n (over ℚ).
Русский
Существуют единица u и показатель n такие, что дискриминант базиса ζ − 1 равен u · p^n (над \mathbb{Q}).
LaTeX
$$$\exists u \in \mathbb{Z}^{\times}, \exists n \in \mathbb{N}, \; \operatorname{discr} \mathbb{Q}(\text{ζ}-1) = u \cdot p^n$$$
Lean4
/-- If `Irreducible (cyclotomic (2 ^ (k + 1)) K)` (in particular for `K = ℚ`), then the norm of
`ζ ^ (2 ^ k) - 1` is `(-2) ^ (2 ^ k)`. -/
theorem norm_pow_sub_one_two {k : ℕ} (hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))) [IsCyclotomicExtension {2 ^ (k + 1)} K L]
(hirr : Irreducible (cyclotomic (2 ^ (k + 1)) K)) : norm K (ζ ^ 2 ^ k - 1) = (-2 : K) ^ 2 ^ k :=
by
have := hζ.pow_of_dvd (fun h => two_ne_zero (pow_eq_zero h)) (pow_dvd_pow 2 (le_succ k))
rw [Nat.pow_div (le_succ k) zero_lt_two, Nat.succ_sub (le_refl k), Nat.sub_self, pow_one] at this
have H : (-1 : L) - (1 : L) = algebraMap K L (-2) :=
by
simp only [map_neg, map_ofNat]
ring
replace hirr : Irreducible (cyclotomic (2 ^ (k + 1)) K) := by simp [hirr]
rw [this.eq_neg_one_of_two_right, H, Algebra.norm_algebraMap, IsCyclotomicExtension.finrank L hirr,
totient_prime_pow Nat.prime_two (zero_lt_succ k), succ_sub_succ_eq_sub, tsub_zero]
simp
