English
Let n be any positive integer and ζ a primitive n-th root of unity in a cyclotomic extension; then the norm of ζ from the extension down to the base field is 1 when n ≠ 2, and is −1 when n = 2.
Русский
Пусть n произвольное положительное целое число, а ζ — примитивный корень единицы порядка n в циклотомическом расширении; тогда норма ζ понизу до базового поля равна 1 при n ≠ 2 и равна −1 при n = 2.
LaTeX
$$$\operatorname{Norm}_{K}(\zeta) = \begin{cases} 1, & n \neq 2 \\ -1, & n = 2 \end{cases}$$$
Lean4
/-- If `Irreducible (cyclotomic n K)` (in particular for `K = ℚ`), the norm of a primitive root is
`1` if `n ≠ 2`. -/
theorem norm_eq_one [IsDomain L] [IsCyclotomicExtension { n } K L] (hn : n ≠ 2) (hirr : Irreducible (cyclotomic n K)) :
norm K ζ = 1 := by
haveI := IsCyclotomicExtension.neZero' n K L
by_cases h1 : n = 1
· rw [h1, one_right_iff] at hζ
rw [hζ, show 1 = algebraMap K L 1 by simp, Algebra.norm_algebraMap, one_pow]
· replace h1 : 2 ≤ n := (two_le_iff n).mpr ⟨NeZero.ne _, h1⟩
rw [← hζ.powerBasis_gen K, PowerBasis.norm_gen_eq_coeff_zero_minpoly, hζ.powerBasis_gen K, ←
hζ.minpoly_eq_cyclotomic_of_irreducible hirr, cyclotomic_coeff_zero K h1, mul_one, hζ.powerBasis_dim K, ←
hζ.minpoly_eq_cyclotomic_of_irreducible hirr, natDegree_cyclotomic]
exact (totient_even <| h1.lt_of_ne hn.symm).neg_one_pow
