coprime_prime_pow
plain-language theorem explainer
Distinct primes p and q raised to any natural powers n and m are coprime. Number theorists building arithmetic functions or Möbius inversion formulas cite this when separating prime-power factors in multiplicative identities. The term proof converts the local Prime predicate to Nat.Prime via the equivalence lemma and hands the claim to the library result coprime_pow_primes.
Claim. If $p$ and $q$ are distinct primes, then for all natural numbers $n$ and $m$, $p^n$ and $q^m$ are coprime, i.e., their greatest common divisor equals 1.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. Prime is a transparent alias for Nat.Prime. The theorem prime_iff states that the local Prime predicate is equivalent to Nat.Prime, allowing direct transfer of standard lemmas. Upstream, primeCounting defines the prime counting function π(n) as the number of primes ≤ n.
proof idea
The term-mode proof extracts Nat.Prime instances from the local Prime hypotheses using the forward direction of prime_iff, then applies the Mathlib lemma Nat.coprime_pow_primes to the exponents, the translated primes, and the inequality hne.
why it matters
This lemma supplies a standard coprimality fact inside the arithmetic functions module that supports Möbius function properties on prime powers. It fills a basic interface need for later Dirichlet algebra work mentioned in the module documentation. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.