primesBelow

Mathlib.NumberTheory.SmoothNumbers

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

English

primesBelow(n) is the set of primes less than n, as a Finset.

Русский

primesBelow(n) — это множество простых чисел меньше n, как Finset.

LaTeX

$$primesBelow(n) = { p ∈ Finset.range(n) | p.Prime }$$

Lean4

/-- `primesBelow n` is the set of primes less than `n` as a `Finset`. -/
def primesBelow (n : ℕ) : Finset ℕ :=
  {p ∈ Finset.range n | p.Prime}

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

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

Разделы

Аффилиация

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