squarefree_ninetyone
plain-language theorem explainer
The declaration asserts that 91 factors as 7 times 13 with no repeated prime factors and therefore satisfies the squarefree predicate. Number theorists building Möbius inversion tools in the arithmetic functions module would cite this fact to confirm μ(91) is nonzero. The proof proceeds as a one-line native_decide call that evaluates the predicate by direct factorization inside the Lean kernel.
Claim. $91$ is squarefree: in the prime factorization $91=7×13$ every exponent equals one.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Squarefree n holds precisely when n has no squared prime divisor, which is the condition equivalent to μ(n)≠0. The local setting keeps such statements minimal before Dirichlet inversion is added on top.
proof idea
The proof is a one-line wrapper that applies native_decide to compute the squarefree predicate for the concrete numeral 91.
why it matters
This supplies a basic verified fact inside the arithmetic-functions layer that supports later Möbius statements such as mobius_ne_zero_iff_squarefree. It aligns with the Recognition Science practice of explicit computational checks before invoking the Recognition Composition Law or the phi-ladder mass formula. No downstream use sites are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.