prime_norm_toInteger_sub_one_of_prime_ne_two

English

In the p^(k+1)-th cyclotomic extension, the subOneIntegralPowerBasis.gen is prime.

Русский

В p^(k+1)-м циклотическим расширении подOneIntegralPowerBasis.gen — простое.

LaTeX

$$$\\operatorname{Prime}\\bigl(h\\zeta.\\text{subOneIntegralPowerBasis}.gen\\bigr)$$$

Lean4

/-- The norm, relative to `ℤ`, of `ζ - 1` in a `p ^ (k + 1)`-th cyclotomic extension of `ℚ` is
a prime if `p ≠ 2`. -/
theorem prime_norm_toInteger_sub_one_of_prime_ne_two [hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K]
    (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) (hodd : p ≠ 2) : Prime (Algebra.norm ℤ (hζ.toInteger - 1)) :=
  by
  have := hζ.norm_toInteger_sub_one_of_prime_ne_two hodd
  simp only at this
  rw [this]
  exact Nat.prime_iff_prime_int.1 hp.out

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