logb_pow

Mathlib.Analysis.SpecialFunctions.Log.Base

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

English

For positive base b ≠ 1 and x real, log_b(b^x) = x.

Русский

Для положительного основания b ≠ 1 и произвольного x: log_b(b^x) = x.

LaTeX

$$$\log_b(b^x) = x$$$

Lean4

theorem logb_pow (b x : ℝ) (k : ℕ) : logb b (x ^ k) = k * logb b x := by rw [logb, logb, log_pow, mul_div_assoc]

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

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

Разделы

Аффилиация

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