coprime_pow_of_prime_not_dvd
plain-language theorem explainer
Number theorists cite this lemma when establishing coprimality between an integer and a prime power during manipulations of the Möbius function or Dirichlet convolution. It asserts that if a prime p does not divide a, then a shares no common prime factors with p raised to any power m. The proof converts the local Prime predicate to Mathlib's Nat.Prime via an equivalence and delegates to the library's standard coprimality result for powers.
Claim. If $p$ is prime and $p$ does not divide the natural number $a$, then $a$ and $p^m$ are coprime for any natural number $m$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. This theorem provides a coprimality fact needed when handling multiplicative functions or squarefree conditions in later statements such as mobius_prime and mobius_apply_of_squarefree. The local Prime predicate is defined as an alias for Nat.Prime, with the equivalence Prime n ↔ Nat.Prime n supplied by prime_iff.
proof idea
The proof first applies the equivalence from prime_iff to obtain Nat.Prime p from the hypothesis Prime p. It then invokes the Mathlib lemma coprime_pow_of_not_dvd directly on the resulting Nat.Prime instance and the non-divisibility hypothesis.
why it matters
This declaration supplies a basic coprimality tool in the arithmetic functions module, supporting subsequent results on the Möbius function such as mobius_prime and mobius_apply_of_squarefree. It fills a standard number-theoretic prerequisite without introducing new Recognition Science structure, though it underpins manipulations that may appear in later Dirichlet algebra layers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.