cardDistinctFactors_eq_zero

Mathlib.NumberTheory.ArithmeticFunction

URI: https://scilib.ai/kg/mathlib#ArithmeticFunction.cardDistinctFactors_eq_zero

English

ω(n) = 0 if and only if n ≤ 1.

Русский

ω(n) = 0 тогда и только тогда, когда n ≤ 1.

LaTeX

$$$$\omega(n) = 0 \iff n \le 1$$$$

Lean4

@[simp]
theorem cardDistinctFactors_eq_zero {n : ℕ} : ω n = 0 ↔ n ≤ 1 := by
  simp [cardDistinctFactors_apply, Nat.le_one_iff_eq_zero_or_eq_one]

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

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

Разделы

Аффилиация

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