English
In a cyclotomic extension with order 2^{k+2}, the norm of ζ − 1 equals (-2)^{2^k}.
Русский
В циклотомическом расширении порядка 2^{k+2} норма ζ − 1 равна (-2)^{2^k}.
LaTeX
$$$\\operatorname{norm}_{\\mathbb{Z}}\\bigl(h\\zeta^{0} - 1\\bigr) = (-2)^{2^{k}}$$$
Lean4
/-- The norm, relative to `ℤ`, of `ζ - 1` in a `2 ^ (k + 2)`-th cyclotomic extension of `ℚ` is `2`.
-/
theorem norm_toInteger_sub_one_of_eq_two_pow {k : ℕ} {K : Type*} [Field K] {ζ : K} [CharZero K]
[IsCyclotomicExtension {2 ^ (k + 2)} ℚ K] (hζ : IsPrimitiveRoot ζ (2 ^ (k + 2))) : norm ℤ (hζ.toInteger - 1) = 2 :=
by
have : NumberField K := IsCyclotomicExtension.numberField {2 ^ (k + 2)} ℚ K
rw [norm_eq_iff ℤ (Sₘ := K) (Rₘ := ℚ) le_rfl, map_sub, map_one, eq_intCast, Int.cast_ofNat, RingOfIntegers.map_mk,
hζ.norm_sub_one_two (Nat.le_add_left 2 k) (Polynomial.cyclotomic.irreducible_rat (Nat.two_pow_pos _))]
