omega_mul_of_coprime
plain-language theorem explainer
The theorem establishes that the distinct-prime-factor counting function ω is additive over coprime nonzero natural numbers, so ω(mn) equals ω(m) plus ω(n) when gcd(m,n) equals 1. Number theorists using arithmetic functions or building multiplicative properties inside the Recognition Science number-theory layer would cite this fact. The proof is a one-line wrapper that unfolds the definition of omega and applies the corresponding Mathlib lemma on cardDistinctFactors.
Claim. Let $m,n$ be nonzero natural numbers with gcd$(m,n)=1$. Then the function ω counting distinct prime factors satisfies ω(mn) = ω(m) + ω(n).
background
The module supplies small wrappers around Mathlib's arithmetic-function library, beginning with the Möbius function μ. The omega function is the standard arithmetic function that returns the number of distinct prime factors of a natural number. The local setting keeps statements lightweight so that deeper Dirichlet algebra and inversion can be added once the basic interfaces are stable.
proof idea
The term proof first simplifies the definition of omega and then applies the Mathlib lemma ArithmeticFunction.cardDistinctFactors_mul on the coprimeness hypothesis.
why it matters
This additivity lemma supplies a standard building block for prime-factor calculations inside the Recognition Science arithmetic-functions module. It supports later work on Möbius inversion and square-free properties listed among the sibling declarations. No downstream uses are recorded yet, so the result remains a foundational interface rather than a direct input to a parent theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.