logb_nat_eq_sum_factorization

Mathlib.Analysis.SpecialFunctions.Log.Base

URI: https://scilib.ai/kg/mathlib#Real.logb_nat_eq_sum_factorization

← MathLib Explorer

English

For n with prime factorization n = ∏ p^t, log_b n equals ∑ t log_b p.

Русский

При факторизации числа n = ∏ p^t имеем log_b n = ∑ t log_b p.

LaTeX

$$$\log_b n = \sum p\in n.factorization,\ t \cdot \log_b p$$$

Lean4

theorem logb_nat_eq_sum_factorization (n : ℕ) : logb b n = n.factorization.sum fun p t => t * logb b p := by
  simp only [logb, mul_div_assoc', log_nat_eq_sum_factorization n, Finsupp.sum, Finset.sum_div]

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

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

Разделы

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

Аффилиация

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