minFac_pos

Mathlib.Data.Nat.Prime.Defs

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

English

For every n, minFac(n) > 0.

Русский

Для каждого n minFac(n) > 0.

LaTeX

$$$\\\\forall n \\\\in \\\\mathbb{N}, \\\\ 0 < \\\\minFac(n).$$$

Lean4

theorem minFac_pos (n : ℕ) : 0 < minFac n := by
  by_cases n1 : n = 1
  · simp [n1]
  · exact (minFac_prime n1).pos

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

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

Разделы

Аффилиация

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