cardFactors_eq_sum_factorization — Mathlib

English

Ω(n) equals the sum of the exponents in the prime factorization of n, i.e., if n = ∏ p^{a_p}, then Ω(n) = ∑ a_p.

Русский

Ω(n) равна сумме показателей степеней в простом разложении n, то есть если n = ∏ p^{a_p}, то Ω(n) = ∑ a_p.

LaTeX

$$$$\Omega(n) = \sum_{p} v_p(n)$$$$

Lean4

theorem cardFactors_eq_sum_factorization {n : ℕ} : Ω n = n.factorization.sum fun _ k => k := by
  simp [cardFactors_apply, ← List.sum_toFinset_count_eq_length, Finsupp.sum]

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