zeta_sub_one_prime — Mathlib

English

Let ζ be a primitive p^(k+1)-th root of unity in a cyclotomic extension over Q. Then the integer hζ.toInteger − 1 is a prime number.

Русский

Пусть ζ — примитивный корень из единиц порядка p^(k+1) в циклотомическом расширении над Q. Тогда целое число hζ.toInteger − 1 является простым.

LaTeX

$$$\\operatorname{Prime}\\bigl(h\\zeta^{\\mathrm{toInteger}} - 1\\bigr)$$$

Lean4

/-- `ζ - 1` is prime if `ζ` is a primitive `p ^ (k + 1)`-th root of unity. -/
theorem zeta_sub_one_prime [IsCyclotomicExtension {p ^ (k + 1)} ℚ K] (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) :
    Prime (hζ.toInteger - 1) := by
  by_cases htwo : p = 2
  · subst htwo
    apply hζ.zeta_sub_one_prime_of_two_pow
  · apply hζ.zeta_sub_one_prime_of_ne_two htwo

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