English
Let p be a prime and hζ a primitive root of order p^(k+1) with IsCyclotomicExtension. If s ≤ k and p^(k−s+1) ≠ 2, then the norm N_K(ζ^{p^s} − 1) equals (p)^{p^s}.
Русский
Пусть p — простое и ζ примитивного порядка p^(k+1) в IsCyclotomicExtension. Если s ≤ k и p^(k−s+1) ≠ 2, то N_K(ζ^{p^s} − 1) = p^{p^s}.
LaTeX
$$$\operatorname{Norm}_{K}(\zeta^{p^s} - 1) = (p)^{p^s}$$$
Lean4
/-- If `Irreducible (cyclotomic (p ^ (k + 1)) K)` (in particular for `K = ℚ`) and `p` is a prime,
then the norm of `ζ ^ (p ^ s) - 1` is `p ^ (p ^ s)` if `p ≠ 2`. -/
theorem norm_pow_sub_one_of_prime_ne_two {k : ℕ} (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) [hpri : Fact p.Prime]
[IsCyclotomicExtension {p ^ (k + 1)} K L] (hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)) {s : ℕ} (hs : s ≤ k)
(hodd : p ≠ 2) : norm K (ζ ^ p ^ s - 1) = (p : K) ^ p ^ s :=
by
refine hζ.norm_pow_sub_one_of_prime_pow_ne_two hirr hs fun h => ?_
rw [← pow_one 2] at h
replace h := eq_of_prime_pow_eq (prime_iff.1 hpri.out) (prime_iff.1 Nat.prime_two) (k - s).succ_pos h
exact hodd h
