Theorems · Theorem · real analysis
Real.exp_log
∀ {x : ℝ}, 0 < x → Real.exp (Real.log x) = x- Cited by
- 58 results in Mathlib
- Foundations
- Depth 171 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- LT.lt.ne'proof · cited by 1,417
- Real.logstatement · cited by 939
- Real.expstatement · cited by 871
- abs_of_posproof · cited by 114
- Real.exp_log_eq_absproof · cited by 7
Cited by59
Results whose statement or proof uses this declaration.
- Real.log_oneproof · cited by 91
- Real.log_expproof · cited by 33
- Real.log_rpowproof · cited by 31
- Complex.exp_logproof · cited by 14
- Real.log_le_log_iffproof · cited by 12
- Real.log_lt_logproof · cited by 10
- Real.log_lt_log_iffproof · cited by 8
- ProbabilityTheory.exp_cgfproof · cited by 8
- Real.log_le_iff_le_expproof · cited by 5
- Real.log_le_sub_one_of_posproof · cited by 5
- Real.le_log_iff_exp_leproof · cited by 5
- Real.expPartialHomeomorphproof · cited by 5