English
For a cyclotomic extension of order p^(k+1) with p ≠ 2, the norm of (hζ.toInteger − 1) is a prime.
Русский
Для циклотомического расширения порядка p^(k+1) с p ≠ 2 норма (hζ.toInteger − 1) простое.
LaTeX
$$Prime\\(\\operatorname{norm}_{\\mathbb{Z}}(h\\zeta^{\\mathrm{toInteger}} - 1)\\)$$
Lean4
/-- We have that `hζ.toInteger - 1` does not divide `2`. -/
theorem toInteger_sub_one_not_dvd_two [IsCyclotomicExtension {p ^ (k + 1)} ℚ K] (hζ : IsPrimitiveRoot ζ (p ^ (k + 1)))
(hodd : p ≠ 2) : ¬hζ.toInteger - 1 ∣ 2 := fun h ↦
by
have : NumberField K := IsCyclotomicExtension.numberField {p ^ (k + 1)} ℚ K
replace h : hζ.toInteger - 1 ∣ (2 : ℤ) := by simp [h]
rw [← Ideal.norm_dvd_iff, hζ.norm_toInteger_sub_one_of_prime_ne_two hodd] at h
· refine hodd <| (prime_dvd_prime_iff_eq ?_ ?_).1 ?_
· exact Nat.prime_iff.1 hp.1
· exact Nat.prime_iff.1 Nat.prime_two
· exact Int.ofNat_dvd.mp h
· rw [hζ.norm_toInteger_sub_one_of_prime_ne_two hodd]
exact Nat.prime_iff_prime_int.1 hp.1
