primorial_pos

Mathlib.NumberTheory.Primorial

URI: https://scilib.ai/kg/mathlib#primorial_pos

English

For any n, n# is positive: 0 < n#.

Русский

Для любого n примориал положителен: 0 < n#.

LaTeX

$$$0 < n\#$$$

Lean4

theorem primorial_pos (n : ℕ) : 0 < n# :=
  prod_pos fun _p hp ↦ (mem_filter.1 hp).2.pos

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

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

Разделы

Аффилиация

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