cardDistinctFactors_one

Mathlib.NumberTheory.ArithmeticFunction

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

English

ω(1) = 0 since 1 has no prime factors.

Русский

ω(1) = 0, так как у 1 нет простых делителей.

LaTeX

$$$$\omega(1) = 0$$$$

Lean4

@[simp]
theorem cardDistinctFactors_one : ω 1 = 0 := by simp [cardDistinctFactors]

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

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

Разделы

Аффилиация

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