`logL_expL`

proved

show as: view math explainer →

module: IndisputableMonolith.Foundation.LogicRealTranscendentals
domain: Foundation
line: 105 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.LogicRealTranscendentals on GitHub at line 105.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 102  exact Real.exp_log hx'
 103
 104/-- Transported logarithm/exponential inverse. -/
 105theorem logL_expL (x : LogicReal) : logL (expL x) = x := by
 106  rw [eq_iff_toReal_eq, toReal_logL, toReal_expL]
 107  exact Real.log_exp _
 108
 109/-- Transported hyperbolic cosine definition. -/
 110theorem coshL_eq_exp (x : LogicReal) :
 111    coshL x = (expL x + expL (-x)) / fromReal 2 := by
 112  rw [eq_iff_toReal_eq, toReal_coshL, toReal_div, toReal_add, toReal_expL,
 113    toReal_expL, toReal_neg, toReal_fromReal]
 114  exact Real.cosh_eq _
 115
 116end
 117
 118end LogicRealTranscendentals
 119end Foundation
 120end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.