squarefree_one'
plain-language theorem explainer
The theorem asserts that the integer 1 satisfies the squarefree predicate. Number theorists working with factorization in the Recognition Science module cite this base case when initializing arguments over the prime set. The proof reduces directly to the standard library result via a single exact application.
Claim. The natural number $1$ is squarefree.
background
The Squarefree module connects the standard Squarefree predicate on naturals to the repo-local valuation vp p n, which extracts the exponent of prime p in n.factorization. The upstream Primes definition supplies the set of all prime naturals as {n | Nat.Prime n}. This supplies the base case for the family of results including squarefree_iff_vp_le_one.
proof idea
The proof is a one-line term wrapper that applies the Mathlib lemma squarefree_one directly.
why it matters
This result supplies the initial case in the squarefree development inside the Primes submodule. It anchors arguments that later feed the EulerInstantiation of primes and the broader number theory used for the phi-ladder and forcing chain steps T5-T8, although no downstream dependents are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.