repunit_four_composite
plain-language theorem explainer
Repunit R_4 equals 1111 and factors explicitly as 11 times 101, establishing compositeness. Number theorists checking small repunit primality or building arithmetic function libraries would cite this factorization. The proof reduces to a single native_decide invocation that verifies the conjunction computationally.
Claim. The integer $1111$ is not prime and satisfies the equality $1111 = 11 × 101$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Local notation in the primes submodule defines Prime as the transparent alias for the standard Nat.Prime predicate on natural numbers. This theorem records a concrete factorization fact for the length-4 repunit inside that setting.
proof idea
One-line wrapper that applies native_decide to discharge the conjunction of non-primality and the explicit factorization equality.
why it matters
The result supplies a verified composite factorization for R_4 in the arithmetic functions module. It populates the primes section of NumberTheory and supports potential later use of arithmetic functions such as Möbius inversion. No parent theorems appear in the used_by edges, and the declaration touches no open scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.