notMem_primesBelow

Mathlib.NumberTheory.SmoothNumbers

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

English

For any n, n ∉ primesBelow(n).

Русский

Для любого n выполняется n ∉ primesBelow(n).

LaTeX

$$$n \notin \mathrm{primesBelow}(n)$$$

Lean4

theorem notMem_primesBelow (n : ℕ) : n ∉ primesBelow n := fun hn ↦ (lt_of_mem_primesBelow hn).false

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

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

Разделы

Аффилиация

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