toInteger_sub_one_dvd_prime' — Mathlib

English

In a cyclotomic extension, the not-existence of integer congruence modulo p holds for primitive root of order p^ (k+1).

Русский

В циклотомическом расширении не существует целого, которое удовлетворяло бы условию по модулю p для примитивного корня порядка p^(k+1).

LaTeX

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

Lean4

/-- In a `p`-th cyclotomic extension of `ℚ`, we have that `ζ - 1` divides `p` in `𝓞 K`. -/
theorem toInteger_sub_one_dvd_prime' [hcycl : IsCyclotomicExtension { p } ℚ K] (hζ : IsPrimitiveRoot ζ p) :
    hζ.toInteger - 1 ∣ p :=
  by
  have : IsCyclotomicExtension {p ^ (0 + 1)} ℚ K := by simpa using hcycl
  replace hζ : IsPrimitiveRoot ζ (p ^ (0 + 1)) := by simpa using hζ
  exact toInteger_sub_one_dvd_prime hζ

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