English
If Irreducible (cyclotomic p^(k+1) K) and p is prime, then the norm N_K(ζ^(p^s) − 1) equals p^(p^s) for s ≤ k with p ≠ 2.
Русский
Если Irreducible (cyclotomic p^(k+1) K) и p простое, тогда нормa N_K(ζ^(p^s) − 1) равна p^(p^s) при s ≤ k и p ≠ 2.
LaTeX
$$$\operatorname{Norm}_{K}(\zeta^{p^s} - 1) = (p)^{p^s}$$$
Lean4
/-- If `Irreducible (cyclotomic (2 ^ k) K)` (in particular for `K = ℚ`) and `k` is at least `2`,
then the norm of `ζ - 1` is `2`. -/
theorem norm_sub_one_two {k : ℕ} (hζ : IsPrimitiveRoot ζ (2 ^ k)) (hk : 2 ≤ k) [H : IsCyclotomicExtension {2 ^ k} K L]
(hirr : Irreducible (cyclotomic (2 ^ k) K)) : norm K (ζ - 1) = 2 :=
by
have : 2 < 2 ^ k := by
nth_rw 1 [← pow_one 2]
exact Nat.pow_lt_pow_right one_lt_two (lt_of_lt_of_le one_lt_two hk)
replace hirr : Irreducible (cyclotomic (2 ^ k) K) := by simp [hirr]
replace hζ : IsPrimitiveRoot ζ (2 ^ k) := by simp [hζ]
obtain ⟨k₁, hk₁⟩ := exists_eq_succ_of_ne_zero (lt_of_lt_of_le zero_lt_two hk).ne.symm
simpa [hk₁] using sub_one_norm_eq_eval_cyclotomic hζ this hirr
