norm_zeta_sub_one_of_isPrimePow — Mathlib

English

If Irreducible (cyclotomic p K) and n is prime with cyclotomic extension, then norm of (zeta p K L − 1) equals p.

Русский

Если Irreducible (cyclotomic p K) и p — простое, тогда норма zeta p K L − 1 равна p.

LaTeX

$$$\operatorname{Norm}_{K}(\zeta_p K L - 1) = p$$$

Lean4

/-- If `IsPrimePow n`, `n ≠ 2` and `Irreducible (cyclotomic n K)` (in particular for `K = ℚ`),
then the norm of `zeta n K L - 1` is `n.minFac`. -/
theorem norm_zeta_sub_one_of_isPrimePow (hn : IsPrimePow n) [IsCyclotomicExtension { n } K L]
    (hirr : Irreducible (cyclotomic n K)) (h : n ≠ 2) : norm K (zeta n K L - 1) = n.minFac :=
  (zeta_spec n K L).sub_one_norm_isPrimePow hn hirr h

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