logb_div

Mathlib.Analysis.SpecialFunctions.Log.Base

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

English

For nonzero x and y, log_b(x/y) = log_b(x) - log_b(y).

Русский

Для x ≠ 0 и y ≠ 0: log_b(x/y) = log_b(x) − log_b(y).

LaTeX

$$$\log_b\left(\frac{x}{y}\right) = \log_b x - \log_b y\quad (x \neq 0, y \neq 0)$$$

Lean4

theorem logb_div (hx : x ≠ 0) (hy : y ≠ 0) : logb b (x / y) = logb b x - logb b y := by
  simp_rw [logb, log_div hx hy, sub_div]

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

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

Разделы

Аффилиация

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