Theorems · Definition · complex analysis
Complex.log
ℂ → ℂ
Inverse of the exp function. Returns values such that (log x).im > - π and (log x).im ≤ π.
log 0 = 0
- Cited by
- 187 results in Mathlib
- Foundations
- Depth 188 from the axioms, rests on 4,755 definitions · 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.
- Complexstatement and proof · cited by 5,565
- Norm.normproof · cited by 5,413
- Complex.ofRealproof · cited by 1,654
- Real.logproof · cited by 939
- Complex.Iproof · cited by 866
- Complex.argproof · cited by 220
Cited by192
Results whose statement or proof uses this declaration.
- Complex.ofReal_cpowproof · cited by 36
- Complex.zero_cpowproof · cited by 29
- Complex.cpow_addproof · cited by 22
- Complex.cpow_oneproof · cited by 20
- Function.Periodic.invQParamproof · cited by 18
- Complex.cpow_zeroproof · cited by 18
- Complex.cpow_negproof · cited by 17
- Complex.ofReal_logstatement and proof · cited by 14
- Complex.exp_logstatement · cited by 14
- Complex.cpow_def_of_ne_zerostatement · cited by 13
- Complex.mul_cpow_ofReal_nonnegproof · cited by 12
- LSeries.logMulproof · cited by 11