not_exists_int_prime_dvd_sub_of_prime_ne_two

English

In a cyclotomic extension, ζ^{instHPow.p (k+1)} is not congruent to any integer modulo p when p^(k+1) ≠ 2.

Русский

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

LaTeX

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

Lean4

/-- In a `p ^ (k + 1)`-th cyclotomic extension of `ℚ `, we have that `ζ` is not congruent to an
  integer modulo `p` if `p ≠ 2`. -/
theorem not_exists_int_prime_dvd_sub_of_prime_ne_two [hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K]
    (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) (hodd : p ≠ 2) : ¬(∃ n : ℤ, (p : 𝓞 K) ∣ (hζ.toInteger - n : 𝓞 K)) :=
  by
  refine not_exists_int_prime_dvd_sub_of_prime_pow_ne_two hζ (fun h ↦ ?_)
  simp_all only [(@Nat.Prime.pow_eq_iff 2 p (k + 1) Nat.prime_two).mp (by assumption_mod_cast), pow_one, ne_eq]

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