not_exists_int_prime_dvd_sub_of_prime_ne_two'

English

If hζ is a primitive root of order p^(k+1) in a cyclotomic extension, the nonexistence of an integer n with p dividing hζ.toInteger − n holds when p^(k+1) ≠ 2.

Русский

Если hζ — примитивный корень порядка p^(k+1) в циклотомическом расширении, то не существует целого n, такого что p делит hζ.toInteger − n, при p^(k+1) ≠ 2.

LaTeX

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

Lean4

/-- In a `p`-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]
    (hζ : IsPrimitiveRoot ζ p) (hodd : p ≠ 2) : ¬(∃ n : ℤ, (p : 𝓞 K) ∣ (hζ.toInteger - n : 𝓞 K)) :=
  by
  have : IsCyclotomicExtension {p ^ (0 + 1)} ℚ K := by simpa using hcycl
  replace hζ : IsPrimitiveRoot ζ (p ^ (0 + 1)) := by simpa using hζ
  exact not_exists_int_prime_dvd_sub_of_prime_ne_two hζ hodd

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