mem_primesBelow

Mathlib.NumberTheory.SmoothNumbers

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

English

For all k,n, n ∈ primesBelow k if and only if n < k and n is prime.

Русский

Для всех k,n верно: n ∈ primesBelow k тогда и только тогда, когда n < k и n простое.

LaTeX

$$n ∈ primesBelow(k) ⇔ n < k ∧ n.Prime$$

Lean4

theorem mem_primesBelow {k n : ℕ} : n ∈ primesBelow k ↔ n < k ∧ n.Prime := by simp [primesBelow]

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

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

Разделы

Аффилиация

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