norm_sub_one_of_prime_ne_two — Mathlib

English

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

Русский

Если hζ — примитивный корень порядка p^(k+1) с простым p и ирреducible циклотомическое, то при любых s ≤ k и p ≠ 2 нормa N_K(ζ^{p^s} − 1) равна p^{p^s}.

LaTeX

$$$\operatorname{Norm}_{K}(\zeta^{p^s} - 1) = (p)^{p^s}$$$

Lean4

/-- If `Irreducible (cyclotomic (p ^ (k + 1)) K)` (in particular for `K = ℚ`) and `p` is an odd
prime, then the norm of `ζ - 1` is `p`. -/
theorem norm_sub_one_of_prime_ne_two {k : ℕ} (hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))) [hpri : Fact p.Prime]
    [IsCyclotomicExtension {p ^ (k + 1)} K L] (hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)) (h : p ≠ 2) :
    norm K (ζ - 1) = p := by simpa using hζ.norm_pow_sub_one_of_prime_ne_two hirr k.zero_le h

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