Theorems · Theorem · complex analysis
Complex.ofReal_log
∀ {x : ℝ}, 0 ≤ x → ↑(Real.log x) = Complex.log ↑x- Cited by
- 14 results in Mathlib
- Foundations
- Depth 191 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites15
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
- Complexstatement · cited by 5,565
- Norm.normproof · cited by 5,413
- Complex.ofRealstatement and proof · cited by 1,654
- Real.logstatement and proof · cited by 939
- Complex.reproof · cited by 882
- Complex.improof · cited by 591
- Complex.logstatement and proof · cited by 187
- Complex.ofReal_reproof · cited by 34
- Complex.extproof · cited by 28
- Complex.norm_of_nonnegproof · cited by 20
- Complex.arg_ofReal_of_nonnegproof · cited by 16
Cited by14
Results whose statement or proof uses this declaration.
- Real.rpow_mulproof · cited by 67
- Complex.ofReal_cpowproof · cited by 36
- Complex.mul_cpow_ofReal_nonnegproof · cited by 12
- Real.rpow_def_of_nonnegproof · cited by 6
- Complex.natCast_logproof · cited by 5
- Real.summable_log_one_add_of_summableproof · cited by 2
- mellin_hasDerivAt_of_isBigO_rpowproof · cited by 2
- Real.tendsto_mul_log_one_add_of_tendstoproof · cited by 2
- Complex.cpow_mul_ofReal_nonnegproof · cited by 2
- Complex.hasDerivAt_Gammaℝ_oneproof · cited by 1
- mellinInv_eq_fourierInvproof · cited by 1
- Complex.GammaIntegral_conjproof · cited by 1