factorization_mul
plain-language theorem explainer
The theorem states that for nonzero natural numbers a and b the prime factorization of their product equals the sum of the individual factorizations. Researchers building cost spectra or phi-rung functions cite it to obtain additivity over products. The proof is a one-line wrapper that invokes the corresponding Mathlib lemma.
Claim. For nonzero natural numbers $a$ and $b$, the prime factorization of $a b$ equals the sum of the prime factorizations of $a$ and of $b$.
background
This module supplies a thin wrapper around Mathlib's Nat.factorization. Its primary goal is to define the repo-local vp function that extracts the exponent of a prime p in n, together with reusable algebraic laws such as vp_mul and vp_pow for downstream work on squarefree numbers and Möbius functions. The local setting is therefore a stable interface that keeps prime-exponent arithmetic explicit while hiding Mathlib internals.
proof idea
The proof is a one-line wrapper that applies the exact tactic to the Mathlib lemma Nat.factorization_mul on the supplied nonzero hypotheses.
why it matters
This result feeds the additivity theorems costSpectrumValue_mul and phiRung_mul, which in turn support J-cost spectra and rung calculations. It therefore supplies the multiplicative decomposition required by the Recognition Composition Law and the phi-ladder mass formula. No open scaffolding questions are closed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.