cardFactors_apply_prime

Mathlib.NumberTheory.ArithmeticFunction

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

English

If p is prime, then Ω(p) = 1.

Русский

Если p — простое число, то Ω(p) = 1.

LaTeX

$$$$\Omega(p) = 1 \quad (p \text{ prime})$$$$

Lean4

@[simp]
theorem cardFactors_apply_prime {p : ℕ} (hp : p.Prime) : Ω p = 1 :=
  cardFactors_eq_one_iff_prime.2 hp

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

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

Разделы

Аффилиация

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