Theorems · Theorem · complex analysis
Complex.hasStrictDerivAt_log
∀ {x : ℂ}, x ∈ Complex.slitPlane → HasStrictDerivAt Complex.log x⁻¹ x- Cited by
- 8 results in Mathlib
- Foundations
- Depth 208 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- Complexstatement and proof · cited by 5,565
- Complex.expproof · cited by 612
- Complex.logstatement and proof · cited by 187
- HasStrictDerivAtstatement · cited by 163
- Complex.slitPlanestatement and proof · cited by 113
- HasStrictDerivAt.congr_simpproof · cited by 41
- Complex.exp_logproof · cited by 14
- Complex.slitPlane_ne_zeroproof · cited by 8
- Complex.hasStrictDerivAt_expproof · cited by 8
- OpenPartialHomeomorph.hasStrictDerivAt_symmproof · cited by 6
- Complex.expOpenPartialHomeomorphproof · cited by 2
Cited by8
Results whose statement or proof uses this declaration.
- Complex.hasDerivAt_logproof · cited by 4
- Complex.hasStrictFDerivAt_log_realproof · cited by 3
- HasDerivAt.clogproof · cited by 1
- HasFDerivAt.clogproof · cited by 1
- HasFDerivWithinAt.clogproof · cited by 1
- HasStrictFDerivAt.clogproof · cited by 1
- HasStrictDerivAt.clogproof · cited by 0
- HasDerivWithinAt.clogproof · cited by 0