logb_neg_eq_logb

Mathlib.Analysis.SpecialFunctions.Log.Base

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

English

The logarithm with the same base is invariant under negation of the argument: log_b(b, -x) = log_b(b, x).

Русский

log_b(b, −x) = log_b(b, x).

LaTeX

$$$\log_b(-x) = \log_b(x)$$$

Lean4

@[simp]
theorem logb_neg_eq_logb (b x : ℝ) : logb b (-x) = logb b x := by rw [← logb_abs b x, ← logb_abs b (-x), abs_neg]

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

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

Разделы

Аффилиация

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