norm_zeta_eq_one — Mathlib

English

If Irreducible (cyclotomic p^(k+1) K) and p prime with cyclotomic extension, then the norm of zeta p K L − 1 is p^(min fac).

Русский

Если Irreducible (cyclotomic p^(k+1) K) и p простое, тогда норма zeta p K L − 1 равна p^{minFac}.

LaTeX

$$$\operatorname{Norm}_{K}(\zeta (p^{k+1}) K L - 1) = p^{\minFac}$$$

Lean4

/-- If `Irreducible (cyclotomic n K)` (in particular for `K = ℚ`), the norm of `zeta n K L` is `1`
if `n` is odd. -/
theorem norm_zeta_eq_one [IsCyclotomicExtension { n } K L] (hn : n ≠ 2) (hirr : Irreducible (cyclotomic n K)) :
    norm K (zeta n K L) = 1 :=
  (zeta_spec n K L).norm_eq_one hn hirr

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