prime_nth_prime

Mathlib.NumberTheory.PrimeCounting

URI: https://scilib.ai/kg/mathlib#Nat.prime_nth_prime

English

The nth prime p_n is prime.

Русский

Пусть p_n обозначает n-ое простое число; само число p_n является простым.

LaTeX

$$$\operatorname{Prime}(p_n)$$$

Lean4

@[simp]
theorem prime_nth_prime (n : ℕ) : Prime (nth Prime n) :=
  nth_mem_of_infinite infinite_setOf_prime _

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru