Documentation

Mathlib.Data.Nat.Prime.Nth

The Nth primes #

source
@[simp]
theorem Nat.nth_prime_zero_eq_two :
Nat.nth Nat.Prime 0 = 2
source
@[deprecated Nat.nth_prime_zero_eq_two]
theorem Nat.zeroth_prime_eq_two :
Nat.nth Nat.Prime 0 = 2

Alias of Nat.nth_prime_zero_eq_two.

source
@[simp]
theorem Nat.nth_prime_one_eq_three :
Nat.nth Nat.Prime 1 = 3