norm_zeta_pow_sub_one_two — Mathlib

English

If hζ is a primitive root of p^(k+1) and p is prime with cyclotomic extension, then the norm of (ζ^(p^s) − 1) equals p^(p^s) for s ≤ k and p ≠ 2.

Русский

Если hζ — примитивный корень порядка p^(k+1) и 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 (2 ^ k) K)` (in particular for `K = ℚ`) and `k` is at least `2`,
then the norm of `zeta (2 ^ k) K L - 1` is `2`. -/
theorem norm_zeta_pow_sub_one_two {k : ℕ} (hk : 2 ≤ k) [IsCyclotomicExtension {2 ^ k} K L]
    (hirr : Irreducible (cyclotomic (2 ^ k) K)) : norm K (zeta (2 ^ k) K L - 1) = 2 :=
  norm_sub_one_two (zeta_spec (2 ^ k) K L) hk hirr

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