prime_fortyone
plain-language theorem explainer
41 is shown to be prime. Number theorists working with Möbius functions or squarefree checks would cite this concrete instance when verifying small primes. The proof is a one-line computational decision that confirms the predicate directly.
Claim. $41$ is a prime number.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. Prime is the transparent alias for the standard natural-number primality predicate. This result supplies a basic concrete fact among the sibling arithmetic-function definitions.
proof idea
One-line wrapper that applies the decide tactic for direct computational verification of the primality predicate.
why it matters
The declaration supplies a basic primality fact inside the arithmetic-functions module. No downstream theorems are recorded, and the result does not connect to Recognition Science landmarks such as the J-uniqueness relation, phi-ladder, or eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.