English
A congruence-based simplification version of the subOneIntegralPowerBasis' generator equality under equal p, k, and ζ.
Русский
Версия упрощения по конгруэнциям равносильна равенству генератора subOneIntegralPowerBasis' при равных p, k и ζ.
LaTeX
$$$$ h\zeta.subOneIntegralPowerBasis' .gen = h\zeta.toInteger - 1 $$$$
Lean4
/-- `ζ - 1` is prime if `p ≠ 2` and `ζ` is a primitive `p ^ (k + 1)`-th root of unity.
See `zeta_sub_one_prime` for a general statement. -/
theorem zeta_sub_one_prime_of_ne_two [IsCyclotomicExtension {p ^ (k + 1)} ℚ K] (hζ : IsPrimitiveRoot ζ (p ^ (k + 1)))
(hodd : p ≠ 2) : Prime (hζ.toInteger - 1) :=
by
letI := IsCyclotomicExtension.numberField {p ^ (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₀ hp.out.one_lt (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]
convert Nat.prime_iff_prime_int.1 hp.out
apply RingHom.injective_int (algebraMap ℤ ℚ)
rw [← Algebra.norm_localization (Sₘ := K) ℤ (nonZeroDivisors ℤ)]
simp only [algebraMap_int_eq, map_natCast]
exact hζ.norm_sub_one_of_prime_ne_two (Polynomial.cyclotomic.irreducible_rat (NeZero.pos _)) hodd
