logb_mul

Mathlib.Analysis.SpecialFunctions.Log.Base

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

English

For nonzero x and y, log_b(xy) = log_b(x) + log_b(y).

Русский

Для x ≠ 0 и y ≠ 0 выполняется log_b(xy) = log_b(x) + log_b(y).

LaTeX

$$$\log_b(xy) = \log_b x + \log_b y\quad (x \neq 0, y \neq 0)$$$

Lean4

theorem logb_mul (hx : x ≠ 0) (hy : y ≠ 0) : logb b (x * y) = logb b x + logb b y := by
  simp_rw [logb, log_mul hx hy, add_div]

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

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

Разделы

Аффилиация

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