primeFactorsList_ne_nil

Mathlib.Data.Nat.Factors

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

English

For n > 1, n.primeFactorsList ≠ [].

Русский

Для n > 1, n.primeFactorsList не пуст.

LaTeX

$$$ n.primeFactorsList \neq [] \iff 1 < n $$$

Lean4

theorem primeFactorsList_ne_nil (n : ℕ) : n.primeFactorsList ≠ [] ↔ 1 < n := by
  simp [primeFactorsList_eq_nil n, one_lt_iff_ne_zero_and_ne_one]

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

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

Разделы

Аффилиация

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