cardFactors_pow

Mathlib.NumberTheory.ArithmeticFunction

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

← MathLib Explorer

English

For any m,k ∈ ℕ, Ω(m^k) = k · Ω(m).

Русский

Для любых m,k ∈ ℕ верно Ω(m^k) = k · Ω(m).

LaTeX

$$$$\Omega(m^k) = k \; \Omega(m)$$$$

Lean4

theorem cardFactors_pow {m k : ℕ} : Ω (m ^ k) = k * Ω m :=
  by
  by_cases hm : m = 0
  · subst hm
    cases k <;> simp
  induction k with
  | zero => simp
  | succ n ih =>
    rw [pow_succ, cardFactors_mul (pow_ne_zero n hm) hm, ih]
    ring

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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