cardFactors_apply_prime_pow

Mathlib.NumberTheory.ArithmeticFunction

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

English

For any prime p and k ∈ ℕ, Ω(p^k) = k.

Русский

Для любого простого p и k ∈ ℕ, Ω(p^k) = k.

LaTeX

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

Lean4

@[simp]
theorem cardFactors_apply_prime_pow {p k : ℕ} (hp : p.Prime) : Ω (p ^ k) = k := by simp [cardFactors_pow, hp]

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

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

Разделы

Аффилиация

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