English
Let hζ be a primitive root of order n. If Irreducible (cyclotomic n K) holds, then the norm of the corresponding primitive root ζ is 1 when n ≠ 2 and is −1 when n = 2.
Русский
Пусть hζ — примитивный корень порядка n. Если irreducible (cyclotomic n K) выполняется, то норма соответствующего примитивного ζ равна 1 при n ≠ 2 и −1 при n = 2.
LaTeX
$$$\operatorname{Norm}_K(\zeta) = \begin{cases} 1, & n \neq 2 \\ -1, & n = 2 \end{cases}$$$
Lean4
/-- If `IsPrimePow n`, `n ≠ 2` and `Irreducible (cyclotomic n K)` (in particular for
`K = ℚ`), then the norm of `ζ - 1` is `n.minFac`. -/
theorem sub_one_norm_isPrimePow (hn : IsPrimePow n) [IsCyclotomicExtension { n } K L]
(hirr : Irreducible (cyclotomic n K)) (h : n ≠ 2) : norm K (ζ - 1) = n.minFac :=
by
have := (lt_of_le_of_ne (succ_le_of_lt (IsPrimePow.one_lt hn)) h.symm)
let hprime : Fact n.minFac.Prime := ⟨minFac_prime (IsPrimePow.ne_one hn)⟩
rw [sub_one_norm_eq_eval_cyclotomic hζ this hirr]
nth_rw 1 [← IsPrimePow.minFac_pow_factorization_eq hn]
obtain ⟨k, hk⟩ : ∃ k, n.factorization n.minFac = k + 1 :=
exists_eq_succ_of_ne_zero
((n.factorization.mem_support_toFun n.minFac).1 <|
mem_primeFactors_iff_mem_primeFactorsList.2 <|
(mem_primeFactorsList (IsPrimePow.ne_zero hn)).2 ⟨hprime.out, minFac_dvd _⟩)
simp [hk]
