Theorems · Theorem · real analysis
Real.log_abs
∀ (x : ℝ), Real.log |x| = Real.log x
- Cited by
- 17 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.
Cites11
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
- absstatement and proof · cited by 1,814
- LT.lt.ne'proof · cited by 1,417
- Real.logstatement and proof · cited by 939
- Real.expproof · cited by 871
- abs_zeroproof · cited by 88
- Real.log_zeroproof · cited by 84
- abs_posproof · cited by 45
- abs_absproof · cited by 19
- Real.exp_log_eq_absproof · cited by 7
- Real.exp_eq_expproof · cited by 6
Cited by17
Results whose statement or proof uses this declaration.
- Real.log_neg_eq_logproof · cited by 27
- Real.tendsto_log_nhdsNE_zeroproof · cited by 8
- Real.posLog_eq_zero_iffproof · cited by 4
- MeromorphicOn.intervalIntegrable_log_normproof · cited by 4
- Real.posLog_eq_logproof · cited by 3
- Real.logb_absproof · cited by 3
- Real.posLog_absproof · cited by 2
- Real.rpow_logb_eq_absproof · cited by 2
- Complex.log_ofReal_reproof · cited by 2
- MeromorphicOn.intervalIntegrable_logproof · cited by 2
- tendsto_log_mul_self_nhdsLT_zeroproof · cited by 2
- circleAverage_log_norm_sub_const_eq_log_radius_add_posLogproof · cited by 1