Part of: The odd primes in order, the mod-4 digit each contributes, the constant they define, and the Chebyshev race sum.
DefinitionoddPrime
For k \ge 0, let p_k denote the k-th odd prime, so p_0 = 3, p_1 = 5,
p_2 = 7, and so on. In Lean this is the (k+1)-st prime in Mathlib's enumeration
(Nat.nth): since the zeroth prime is 2, shifting the index by one skips exactly the prime
2.
Lean code for Definition oddPrime
-
⟲
def oddPrime (k
ℕ: ℕNat : TypeThe natural numbers, starting at zero. This type is special-cased by both the kernel and the compiler, and overridden with an efficient implementation. Both use a fast arbitrary-precision arithmetic library (usually [GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.) : ℕNat : TypeThe natural numbers, starting at zero. This type is special-cased by both the kernel and the compiler, and overridden with an efficient implementation. Both use a fast arbitrary-precision arithmetic library (usually [GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.def oddPrime (k
ℕ: ℕNat : TypeThe natural numbers, starting at zero. This type is special-cased by both the kernel and the compiler, and overridden with an efficient implementation. Both use a fast arbitrary-precision arithmetic library (usually [GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.) : ℕNat : TypeThe natural numbers, starting at zero. This type is special-cased by both the kernel and the compiler, and overridden with an efficient implementation. Both use a fast arbitrary-precision arithmetic library (usually [GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
⟲:= Nat.nthNat.nth (p : ℕ → Prop) (n : ℕ) : ℕFind the `n`-th natural number satisfying `p` (indexed from `0`, so `nth p 0` is the first
natural number satisfying `p`), or `0` if there is no such number. See also
`Subtype.orderIsoOfNat` for the order isomorphism with ℕ when `p` is infinitely often true. Nat.PrimeNat.Prime (p : ℕ) : Prop`Nat.Prime p` means that `p` is a prime number, that is, a natural number
at least 2 whose only divisors are `p` and `1`.
The theorem `Nat.prime_def` witnesses this description of a prime number. (kℕ + 1ℕ)