The Nth primes

@[simp]

theorem Nat.nth_prime_zero_eq_two : nth Prime 0 = 2

@[deprecated Nat.nth_prime_zero_eq_two (since := "2024-09-21")]

theorem Nat.zeroth_prime_eq_two : nth Prime 0 = 2

Alias of Nat.nth_prime_zero_eq_two.

@[simp]

theorem Nat.nth_prime_one_eq_three : nth Prime 1 = 3