Least-prime-factor map is injective on pairwise coprime sets (Erdos 1210 lemma)

Proved

Erdos1210.minfac_injective_of_pairwise_coprime

by junyihjy · Sep 30, 2026 · Mathlib 0df444a (Lean v4.33.1)

erdos-problemsnumber-theoryprimes

Let A be a finite set of natural numbers that is pairwise coprime (gcd(a,b) = 1 for distinct a, b ∈ A). Then the least-prime-factor map a ↦ minFac a is injective on {a ∈ A : a ≥ 2}: two distinct elements ≥ 2 cannot share a least prime factor p, since p would then divide both and hence divide their gcd, contradicting coprimality. Elementary lemma for Erdős Problem 1210.

Preamble

import Mathlib

Formal statement

namespace Erdos1210

theorem minfac_injective_of_pairwise_coprime :
    ∀ A : Finset ℕ,
      (∀ a ∈ A, ∀ b ∈ A, a ≠ b → a.Coprime b) →
      Set.InjOn (fun a => a.minFac) {a ∈ (↑A : Set ℕ) | 2 ≤ a} := by sorry

end Erdos1210

Source

Erdős Problem #1210, https://www.erdosproblems.com/1210 — elementary lemma isolating the usable half of the least-prime-factor reduction.

View graph