mod4_nineteen_prime
plain-language theorem explainer
19 is established as prime and congruent to 3 modulo 4. Number theorists applying arithmetic functions such as the Möbius function to primes ≡3 mod 4 would cite this concrete case. The proof is a one-line term that invokes native_decide to evaluate the conjunction directly.
Claim. $19$ is prime and $19 ≡ 3 mod 4$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. Prime is defined as a transparent alias for Nat.Prime. The upstream alias allows the theorem to combine primality with the modular condition in a single statement.
proof idea
The proof is a one-line wrapper that applies native_decide to the conjunction of the primality predicate and the modular equality.
why it matters
This supplies a specific prime fact inside the arithmetic functions module for use in Möbius calculations. It fills a basic number-theoretic need without direct ties to the forcing chain or Recognition Composition Law. No downstream uses appear in the current graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.