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

@[simp]

theorem Nat.nth_prime_two_eq_five : nth Prime 2 = 5

@[simp]

theorem Nat.nth_prime_three_eq_seven : nth Prime 3 = 7

@[simp]

theorem Nat.nth_prime_four_eq_eleven : nth Prime 4 = 11