exp_log_eq_abs

Mathlib.Analysis.SpecialFunctions.Log.Basic

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

← MathLib Explorer

English

For x ≠ 0, exp(log x) equals the absolute value |x|.

Русский

Для x ≠ 0 верно exp(log x) = |x|.

LaTeX

$$$x \neq 0 \Rightarrow \exp(\log x) = |x|$$$

Lean4

theorem exp_log_eq_abs (hx : x ≠ 0) : exp (log x) = |x| := by
  rw [log_of_ne_zero hx, ← coe_expOrderIso_apply, OrderIso.apply_symm_apply, Subtype.coe_mk]

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

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

Разделы

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

Аффилиация

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