cardFactors_apply

Mathlib.NumberTheory.ArithmeticFunction

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

English

If p is prime and k ≥ 0, then Ω(p^k) = k, since p appears with multiplicity k in the factorization.

Русский

Если p — простое число и k ≥ 0, то Ω(p^k) = k, так как p встречается с кратностью k в разложении числа.

LaTeX

$$$$\Omega(p^k) = k\quad(\text{for prime } p),$$$$

Lean4

theorem cardFactors_apply {n : ℕ} : Ω n = n.primeFactorsList.length :=
  rfl

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

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

Разделы

Аффилиация

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