prime_norm_toInteger_sub_one_of_prime_pow_ne_two

English

In a cyclotomic extension of order p^(k+1) with p^(k+1) ≠ 2, the element ζ−1 is not congruent to any integer modulo p.

Русский

В циклотомическом расширении порядка p^(k+1) при p^(k+1) ≠ 2, ζ−1 не эквивалентно ни одному целому числу по модулю p.

LaTeX

$$¬∃ n ∈ ℤ, (p : 𝒪K) ∣ (hζ.toInteger − n)$$

Lean4

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

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