logb_rpow_eq_mul_logb_of_pos

Mathlib.Analysis.SpecialFunctions.Log.Base

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

English

For any base b and exponent k ∈ N, log_b(x^k) = k log_b(x).

Русский

Для любого основания b и целого k≥0: log_b(x^k) = k log_b(x).

LaTeX

$$$\log_b(x^k) = k \cdot \log_b x\quad (k \in \mathbb{N})$$$

Lean4

theorem logb_rpow_eq_mul_logb_of_pos (hx : 0 < x) : logb b (x ^ y) = y * logb b x := by
  rw [logb, log_rpow hx, logb, mul_div_assoc]

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

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

Разделы

Аффилиация

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