zeta_sub_one_prime' — Mathlib

English

Let hζ be a primitive p-th root of unity in a cyclotomic extension over Q. Then hζ.toInteger − 1 is prime.

Русский

Пусть hζ будет примитивным p-орбитным корнем единства в циклотомическом расширении над Q. Тогда hζ.toInteger − 1 простое.

LaTeX

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

Lean4

/-- `ζ - 1` is prime if `ζ` is a primitive `p`-th root of unity. -/
theorem zeta_sub_one_prime' [h : IsCyclotomicExtension { p } ℚ K] (hζ : IsPrimitiveRoot ζ p) :
    Prime ((hζ.toInteger - 1)) :=
  by
  convert zeta_sub_one_prime (k := 0) (by simpa only [zero_add, pow_one])
  simpa only [zero_add, pow_one]

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