norm_toInteger_pow_sub_one_of_two

English

If s ≤ k, and p^(k−s+1) ≠ 2, then the norm of (ζ^{p^s} − 1) in ℤ equals p^{p^s}.

Русский

Если s ≤ k и p^{k−s+1} ≠ 2, то норма (ζ^{p^s} − 1) в ℤ равна p^{p^s}.

LaTeX

$$$\\operatorname{norm}_{\\mathbb{Z}}\\bigl(h\\zeta^{p^{s}} - 1\\bigr) = p^{p^{s}}$$$

Lean4

/-- The norm, relative to `ℤ`, of `ζ ^ 2 ^ k - 1` in a `2 ^ (k + 1)`-th cyclotomic extension of `ℚ`
is `(-2) ^ 2 ^ k`. -/
theorem norm_toInteger_pow_sub_one_of_two [IsCyclotomicExtension {2 ^ (k + 1)} ℚ K]
    (hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))) : Algebra.norm ℤ (hζ.toInteger ^ 2 ^ k - 1) = (-2) ^ 2 ^ k :=
  by
  have : NumberField K := IsCyclotomicExtension.numberField {2 ^ (k + 1)} ℚ K
  rw [Algebra.norm_eq_iff ℤ (Sₘ := K) (Rₘ := ℚ) le_rfl]
  simp [hζ.norm_pow_sub_one_two (cyclotomic.irreducible_rat (pow_pos (by decide) _))]

Похожие утверждения