FenchelNielsenZomorrodian/Discrete/Arithmetic/PrimeDivisors.lean
1import Mathlib.Data.Nat.Prime.Basic
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FenchelNielsenZomorrodian/Discrete/Arithmetic/PrimeDivisors.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Arithmetic of period families
14GCD, LCM, prime-divisor, replicated-family, and abelian-period numerical lemmas used in compact zero-genus reductions.
15-/
17namespace FenchelNielsen
20 {ι : Type*} {periods : ι → ℕ} :
21 (¬ ∀ i j, i ≠ j → Nat.Coprime (periods i) (periods j)) ↔
22 ∃ p : ℕ, p.Prime ∧
23 ∃ i j : ι, i ≠ j ∧ p ∣ periods i ∧ p ∣ periods j := by
24 constructor
25 · intro hNot
26 by_contra hPrime
27 apply hNot
28 intro i j hij
29 by_contra hCoprime
30 rcases Nat.Prime.not_coprime_iff_dvd.mp hCoprime with ⟨p, hp, hpi, hpj⟩
31 exact hPrime ⟨p, hp, i, j, hij, hpi, hpj⟩
32 · rintro ⟨p, hp, i, j, hij, hpi, hpj⟩
33 intro hPair
34 exact (Nat.Prime.not_coprime_iff_dvd.mpr ⟨p, hp, hpi, hpj⟩) (hPair i j hij)
36end FenchelNielsen