prime_sixhundredfortyone
plain-language theorem explainer
641 is established as a prime integer, noted for dividing the fifth Fermat number. Number theorists examining Fermat primes or exact factorization facts would reference this result. The verification is a direct computational decision via native_decide.
Claim. The positive integer 641 is prime.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, starting with the Möbius function μ. Prime is the repo-local alias for Nat.Prime. The declaration sits in the Primes section of NumberTheory and supplies a concrete fact used in arithmetic computations.
proof idea
The proof is a one-line wrapper that applies native_decide to confirm primality of 641 by direct computation.
why it matters
The result supplies a verified prime fact tied to Fermat-number factorization inside the NumberTheory.Primes layer. It supports exact arithmetic steps that later feed into Möbius inversion and square-free checks, though it currently has no downstream citations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.