coprime_pow_right_iff
plain-language theorem explainer
The theorem asserts that for positive integer n and natural numbers a, b, a shares no common prime factors with b to the power n precisely when it shares none with b. Number theorists applying Möbius inversion or squarefree characterizations in prime factorization contexts would cite this equivalence to simplify gcd arguments. The proof is a direct one-line term application of the standard coprimality lemma for right powers in the naturals library.
Claim. For positive integer $n$ and natural numbers $a, b$, $a$ is coprime to $b^n$ if and only if $a$ is coprime to $b$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function for squarefree and inversion properties. Coprimality here means gcd equals one, a standard notion used to characterize when two numbers share no prime factors. The local setting keeps statements minimal so that Dirichlet algebra can be added once basic interfaces stabilize.
proof idea
The proof is a one-line wrapper that applies the coprimality preservation lemma for right powers directly to the given hypotheses.
why it matters
This result supplies a basic equivalence needed for arithmetic function development in the primes module, supporting Möbius applications and squarefree checks that feed into Recognition Science number-theoretic foundations. It aligns with the framework's use of prime-related constants and the phi-ladder mass formula by enabling clean factorization arguments. No downstream parents are recorded yet, leaving it as an available utility for later inversion or ladder constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.