norm_toInteger_pow_sub_one_of_prime_pow_ne_two

English

For primitive root ζ of order p, hζ.toInteger − 1 is prime.

Русский

Для примитивного корня ζ порядка p, hζ.toInteger − 1 простое.

LaTeX

$$$\\operatorname{Prime}\\left(h\\zeta^{\\mathrm{toInteger}} - 1\\right)$$$

Lean4

/-- The norm, relative to `ℤ`, of `ζ ^ p ^ s - 1` in a `p ^ (k + 1)`-th cyclotomic extension of `ℚ`
is p ^ p ^ s` if `s ≤ k` and `p ^ (k - s + 1) ≠ 2`. -/
theorem norm_toInteger_pow_sub_one_of_prime_pow_ne_two [IsCyclotomicExtension {p ^ (k + 1)} ℚ K]
    (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) {s : ℕ} (hs : s ≤ k) (htwo : p ^ (k - s + 1) ≠ 2) :
    Algebra.norm ℤ (hζ.toInteger ^ p ^ s - 1) = p ^ p ^ s :=
  by
  have : NumberField K := IsCyclotomicExtension.numberField {p ^ (k + 1)} ℚ K
  rw [Algebra.norm_eq_iff ℤ (Sₘ := K) (Rₘ := ℚ) le_rfl]
  simp [hζ.norm_pow_sub_one_of_prime_pow_ne_two (cyclotomic.irreducible_rat (NeZero.pos _)) hs htwo]

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