nonempty_primeFactors

Mathlib.Data.Nat.PrimeFin

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

← MathLib Explorer

English

The prime factors of n are nonempty exactly when n > 1.

Русский

Множество простых делителей числа n непусто тогда, когда n > 1.

LaTeX

$$$ n.primeFactors.Nonempty \\iff 1 < n $$$

Lean4

@[simp]
theorem nonempty_primeFactors {n : ℕ} : n.primeFactors.Nonempty ↔ 1 < n := by
  rw [← not_iff_not, Finset.not_nonempty_iff_eq_empty, primeFactors_eq_empty, not_lt, Nat.le_one_iff_eq_zero_or_eq_one]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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