FenchelNielsenZomorrodian.Discrete.Arithmetic.PrimeDivisors
This module studies prime divisors for fenchel nielsen zomorrodian. A period family is not pairwise coprime exactly when some prime divides two distinct periods.
import
- Mathlib.Data.Nat.Prime.Basic
theorem not_pairwiseCoprimeFamily_iff_exists_prime_dvd_two
{ι : Type*} {periods : ι → ℕ} :
(¬ ∀ i j, i ≠ j → Nat.Coprime (periods i) (periods j)) ↔
∃ p : ℕ, p.Prime ∧
∃ i j : ι, i ≠ j ∧ p ∣ periods i ∧ p ∣ periods jA period family is not pairwise coprime exactly when some prime divides two distinct periods.
Show proof
by
constructor
· intro hNot
by_contra hPrime
apply hNot
intro i j hij
by_contra hCoprime
rcases Nat.Prime.not_coprime_iff_dvd.mp hCoprime with ⟨p, hp, hpi, hpj⟩
exact hPrime ⟨p, hp, i, j, hij, hpi, hpj⟩
· rintro ⟨p, hp, i, j, hij, hpi, hpj⟩
intro hPair
exact (Nat.Prime.not_coprime_iff_dvd.mpr ⟨p, hp, hpi, hpj⟩) (hPair i j hij)Proof. Unfold the arithmetic, signature, quotient, or subgroup definition named in the statement. The result is a direct numerical, topological, or kernel-property calculation rather than a generic presentation-relator check.
□