superprime_fortyone
plain-language theorem explainer
Both 41 and 13 satisfy the definition of primality. Researchers computing Möbius values or populating small-rung entries on the phi-ladder would cite the fact when they need verified primes inside arithmetic-function identities. The proof is a one-line native decision that evaluates the two Nat.Prime predicates directly.
Claim. $41$ and $13$ are both prime numbers.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Prime is the transparent alias for Nat.Prime. Upstream material includes the Basic.Prime abbreviation and several “is” structures from foundation modules that certify algebraic or collision-free properties, though the present theorem invokes them only through the decidability of primality.
proof idea
Term-mode proof consisting of a single native_decide application. The tactic evaluates the conjunction Prime 41 ∧ Prime 13 by direct computation of the underlying Nat.Prime predicates.
why it matters
The result supplies concrete small primes needed for Möbius evaluations and square-free checks inside the same module. It sits in the NumberTheory.Primes section that prepares arithmetic tools for later Dirichlet inversion and phi-ladder mass formulas. No downstream uses are recorded, so the declaration functions as a verified constant for the arithmetic-function layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.