cosh_eq — Mathlib

English

For every real x, cosh x equals (e^x + e^{-x})/2.

Русский

Для любого вещественного x: cosh x = (e^x + e^{-x})/2.

LaTeX

$$$\\cosh x = \\frac{e^x + e^{-x}}{2}$$$

Lean4

/-- The definition of `cosh` in terms of `exp`. -/
theorem cosh_eq (x : ℝ) : cosh x = (exp x + exp (-x)) / 2 :=
  eq_div_of_mul_eq two_ne_zero <| by
    rw [cosh, exp, exp, Complex.ofReal_neg, Complex.cosh, mul_two, ← Complex.add_re, ← mul_two,
      div_mul_cancel₀ _ (two_ne_zero' ℂ), Complex.add_re]

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