English
If Irreducible (cyclotomic (p^(k+1)) K) and p is prime with cyclotomic extension, then the norm of ζ^(p^s) − 1 is p^(p^s) for s ≤ k and p ≠ 2.
Русский
Если ирреducible (cyclotomic (p^(k+1)) K) и p простое, то нормa ζ^(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 (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 `k ≠ 0` and `s ≤ k`. -/
theorem norm_pow_sub_one_eq_prime_pow_of_ne_zero {k s : ℕ} (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) [hpri : Fact p.Prime]
[hcycl : IsCyclotomicExtension {p ^ (k + 1)} K L] (hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)) (hs : s ≤ k)
(hk : k ≠ 0) : norm K (ζ ^ p ^ s - 1) = (p : K) ^ p ^ s :=
by
by_cases htwo : p ^ (k - s + 1) = 2
· have hp : p = 2 := by
rw [← pow_one 2] at htwo
exact eq_of_prime_pow_eq (prime_iff.1 hpri.out) (prime_iff.1 Nat.prime_two) (succ_pos _) htwo
replace hs : s = k := by
rw [hp] at htwo
nth_rw 2 [← pow_one 2] at htwo
replace htwo := Nat.pow_right_injective rfl.le htwo
rw [add_eq_right, Nat.sub_eq_zero_iff_le] at htwo
exact le_antisymm hs htwo
simp only [hp, hs] at hζ hirr hcycl ⊢
obtain ⟨k₁, hk₁⟩ := Nat.exists_eq_succ_of_ne_zero hk
rw [hζ.norm_pow_sub_one_two hirr, hk₁, _root_.pow_succ', pow_mul, neg_eq_neg_one_mul, mul_pow, neg_one_sq, one_mul,
← pow_mul, ← _root_.pow_succ']
simp
· exact hζ.norm_pow_sub_one_of_prime_pow_ne_two hirr hs htwo
