English
For x ≠ 0, exp(log x) = x.
Русский
Для x ≠ 0 выполняется exp(log x) = x.
LaTeX
$$$\exp(\log x) = x \quad (x \neq 0).$$$
Lean4
theorem exp_log {x : ℂ} (hx : x ≠ 0) : exp (log x) = x := by
rw [log, exp_add_mul_I, ← ofReal_sin, sin_arg, ← ofReal_cos, cos_arg hx, ← ofReal_exp,
Real.exp_log (norm_pos_iff.mpr hx), mul_add, ofReal_div, ofReal_div,
mul_div_cancel₀ _ (ofReal_ne_zero.2 <| norm_ne_zero_iff.mpr hx), ← mul_assoc,
mul_div_cancel₀ _ (ofReal_ne_zero.2 <| norm_ne_zero_iff.mpr hx), re_add_im]