prime_of_mem_primesBelow

Mathlib.NumberTheory.SmoothNumbers

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

English

Let p,n ∈ ℕ. If p ∈ primesBelow(n), then p is prime.

Русский

Пусть p,n ∈ ℕ. Если p ∈ primesBelow(n), то p простое.

LaTeX

$$$p \in \mathrm{primesBelow}(n) \Rightarrow \mathrm{Prime}(p)$$$

Lean4

theorem prime_of_mem_primesBelow {p n : ℕ} (h : p ∈ n.primesBelow) : p.Prime :=
  (Finset.mem_filter.mp h).2

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

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

Разделы

Аффилиация

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