English
Let ζ be a primitive 2^{k+1}-th root of unity. Then the integer associated to ζ minus 1 is a prime number.
Русский
Пусть ζ — примитивный корень единицы порядка 2^{k+1}. Тогда число, связанное с ζ, минус единица, является простым.
LaTeX
$$$\\\\forall \\\\zeta \,\\\\big( \\\\operatorname{ord}(\\\\zeta) = 2^{k+1} \\\\wedge \\\\zeta^{2^{k+1}} = 1 \\\\Rightarrow \\\\operatorname{Prime}(\\\\toInteger(\\\\zeta) - 1) \\\\bigr)$$$
Lean4
/-- `ζ - 1` is prime if `ζ` is a primitive `2 ^ (k + 1)`-th root of unity.
See `zeta_sub_one_prime` for a general statement. -/
theorem zeta_sub_one_prime_of_two_pow [IsCyclotomicExtension {2 ^ (k + 1)} ℚ K] (hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))) :
Prime (hζ.toInteger - 1) :=
by
have := IsCyclotomicExtension.numberField {2 ^ (k + 1)} ℚ K
refine Ideal.prime_of_irreducible_absNorm_span (fun h ↦ ?_) ?_
· apply hζ.pow_ne_one_of_pos_of_lt one_ne_zero (one_lt_pow₀ (by decide) (by simp))
rw [sub_eq_zero] at h
simpa using congrArg (algebraMap _ K) h
rw [Nat.irreducible_iff_prime, Ideal.absNorm_span_singleton, ← Nat.prime_iff, ← Int.prime_iff_natAbs_prime]
cases k
· convert Prime.neg Int.prime_two
apply RingHom.injective_int (algebraMap ℤ ℚ)
rw [← Algebra.norm_localization (Sₘ := K) ℤ (nonZeroDivisors ℤ)]
simp only [algebraMap_int_eq, map_neg, map_ofNat]
simpa only [zero_add, pow_one, AddSubgroupClass.coe_sub, OneMemClass.coe_one, pow_zero] using
hζ.norm_pow_sub_one_two (cyclotomic.irreducible_rat (by simp only [zero_add, pow_one, Nat.ofNat_pos]))
convert Int.prime_two
apply RingHom.injective_int (algebraMap ℤ ℚ)
rw [← Algebra.norm_localization (Sₘ := K) ℤ (nonZeroDivisors ℤ), algebraMap_int_eq]
exact hζ.norm_sub_one_two Nat.AtLeastTwo.prop (cyclotomic.irreducible_rat (by simp))
