prime_fortythree
plain-language theorem explainer
The declaration asserts that 43 is prime. Number theorists checking small cases in arithmetic functions would cite it when confirming square-freeness or Möbius values at 43. The proof proceeds by a single decision procedure that evaluates the primality predicate directly.
Claim. The natural number 43 is prime.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. The local setting keeps statements minimal pending deeper Dirichlet algebra. The upstream alias defines Prime as the standard Nat.Prime predicate on natural numbers.
proof idea
The proof is a one-line wrapper that applies the decide tactic to evaluate the decidable proposition Prime 43.
why it matters
This supplies a verified small-prime fact inside the arithmetic-functions module. It supports basic checks that may feed later Möbius or square-free lemmas, though no downstream uses are recorded yet and no direct tie to the forcing chain or phi-ladder is present.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.