prime_norm_toInteger_sub_one_of_prime_ne_two'

English

If p ≠ 2, then the norm of (hζ.toInteger − 1) equals p when the extension is cyclotomic of order p.

Русский

Если p ≠ 2, норма (hζ.toInteger − 1) равна p для циклотомического порядка p.

LaTeX

$$$\\operatorname{norm}_{\\mathbb{Z}}\\bigl(h\\zeta^{\\mathrm{toInteger}} - 1\\bigr) = p$$$

Lean4

/-- The norm, relative to `ℤ`, of `ζ - 1` in a `p`-th cyclotomic extension of `ℚ` is a prime if
`p ≠ 2`. -/
theorem prime_norm_toInteger_sub_one_of_prime_ne_two' [hcycl : IsCyclotomicExtension { p } ℚ K]
    (hζ : IsPrimitiveRoot ζ p) (hodd : p ≠ 2) : Prime (Algebra.norm ℤ (hζ.toInteger - 1)) :=
  by
  have : IsCyclotomicExtension {p ^ (0 + 1)} ℚ K := by simpa using hcycl
  replace hζ : IsPrimitiveRoot ζ (p ^ (0 + 1)) := by simpa using hζ
  exact hζ.prime_norm_toInteger_sub_one_of_prime_ne_two hodd

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