log_inv

Mathlib.Analysis.SpecialFunctions.Log.Basic

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

← MathLib Explorer

English

For any nonzero x, log(x^{-1}) = - log x.

Русский

Для любого ненулевого x имеет log(x^{-1}) = −log x.

LaTeX

$$$$ \log(x^{-1}) = -\log x \quad \text{for } x \neq 0.$$$$

Lean4

@[simp]
theorem log_inv (x : ℝ) : log x⁻¹ = -log x := by
  by_cases hx : x = 0; · simp [hx]
  rw [← exp_eq_exp, exp_log_eq_abs (inv_ne_zero hx), exp_neg, exp_log_eq_abs hx, abs_inv]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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