coprime_pow_left_iff
plain-language theorem explainer
Coprimality between a natural number a raised to a positive power n and b holds exactly when a and b share no common prime factors. Number theorists working with arithmetic functions and Möbius inversion would cite this equivalence to simplify exponentiated coprimality checks. The proof is a one-line wrapper applying the corresponding Mathlib lemma directly.
Claim. For positive integer $n$ and natural numbers $a,b$, $a^n$ and $b$ are coprime if and only if $a$ and $b$ are coprime.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ for later Dirichlet inversion work. Coprimality statements support multiplicative properties and squarefree checks in this setting. Upstream results include collision-free class definitions and algebraic tautology theorems that maintain consistency across foundational components.
proof idea
The proof is a one-line wrapper that applies the Mathlib lemma Nat.coprime_pow_left_iff.
why it matters
This equivalence supplies a basic tool inside the arithmetic functions module for handling powers in coprimality arguments. It supports sibling results on the Möbius function and squarefree conditions without feeding any listed parent theorems. No direct tie to Recognition Science chain steps such as T5 J-uniqueness or the phi-ladder appears here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.