squarefree_mul_of_coprime
plain-language theorem explainer
The product of two coprime squarefree natural numbers is squarefree. Number theorists working with prime factorizations or squarefree decompositions cite this when composing such integers multiplicatively. The proof is a one-line wrapper applying the Mathlib lemma Nat.squarefree_mul to the coprimality hypothesis and the pair of squarefree assumptions.
Claim. Let $m, n$ be square-free natural numbers with $m$ and $n$ coprime. Then the product $m n$ is square-free.
background
The module defines squarefreeness on naturals via the standard predicate and links it to the local valuation vp p n, the exponent of prime p in n.factorization. Squarefree holds precisely when vp p n ≤ 1 for every prime p. This lemma belongs to a cluster of siblings that characterize the predicate through valuations, including squarefree_iff_vp_le_one and squarefree_vp_dichotomy. The module setting is purely number-theoretic and supplies multiplicative closure properties needed for later factorization arguments.
proof idea
One-line wrapper that applies the Mathlib lemma Nat.squarefree_mul to the coprimality hypothesis and then uses the pair of squarefree assumptions on m and n via the right-to-left direction of the equivalence.
why it matters
The result supplies a basic multiplicative closure fact inside the Squarefree module, which underpins clean factorization statements used across the Recognition Science number-theory layer. It aligns with the need for controlled products in the phi-ladder constructions and mass formulas that rely on squarefree building blocks. No downstream uses are recorded yet, so the lemma functions as a utility step rather than a direct feeder to a parent theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.