squarefree_thirty
plain-language theorem explainer
The declaration asserts that the integer 30 has no squared prime factors in its factorization. Number theorists applying Möbius inversion or arithmetic functions to small composites would cite this when verifying squarefreeness for basic computations. The proof is a direct computational check via a native decision procedure.
Claim. $30$ is squarefree.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Squarefreeness of an integer n holds precisely when μ(n) is nonzero, per the sibling definitions such as mobius_ne_zero_iff_squarefree. This local setting keeps statements basic before adding Dirichlet algebra. The upstream results supply supporting structures from Foundation and GameTheory modules for empirical programs and mechanism design.
proof idea
The proof is a one-line term that applies the native_decide tactic to verify the squarefreeness of 30 by direct computation.
why it matters
This result supplies a verified basic fact for the arithmetic functions module and its Möbius footholds. It contributes to the NumberTheory.Primes section without linkage to the forcing chain T0-T8, RCL, or physical constants. No downstream uses appear in the current graph and no open questions are addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.