prime_fourhundredfortynine
plain-language theorem explainer
449 is established as a prime natural number. Number theorists applying arithmetic functions such as the Möbius function would reference this fact for small-prime checks inside the module. The proof reduces the statement to a single native_decide call that executes the decidable primality procedure.
Claim. $449$ is a prime number.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, starting with the Möbius function μ. Prime is the transparent alias for Nat.Prime. The local setting keeps statements minimal so that Dirichlet inversion and related algebra can be added once the basic interfaces stabilize.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to the primality predicate, discharging the goal by direct computation.
why it matters
The result supplies a concrete prime instance inside the arithmetic-functions file that supports Möbius and related calculations. It sits in the NumberTheory.Primes layer of the monolith and fills a basic fact needed for any later use of square-free or multiplicative functions. No downstream theorems currently cite it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.