Theorems · Theorem · real analysis
Complex.hasStrictDerivAt_const_cpow
∀ {x y : ℂ}, x ≠ 0 ∨ y ≠ 0 → HasStrictDerivAt (fun y => x ^ y) (x ^ y * Complex.log x) y- Cited by
- 6 results in Mathlib
- Foundations
- Depth 201 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites20
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Set.ofPredproof · cited by 6,101
- Complexstatement and proof · cited by 5,565
- mul_oneproof · cited by 3,885
- MulZeroClass.mul_zeroproof · cited by 2,091
- Filter.Eventually.monoproof · cited by 646
- Complex.expproof · cited by 612
- Complex.logstatement and proof · cited by 187
- HasStrictDerivAtstatement and proof · cited by 163
- emproof · cited by 115
- HasStrictDerivAt.congr_simpproof · cited by 41
- Complex.zero_cpowproof · cited by 29
- IsOpen.eventually_memproof · cited by 24
Cited by6
Results whose statement or proof uses this declaration.
- HasDerivAt.const_cpowproof · cited by 4
- HasDerivWithinAt.const_cpowproof · cited by 1
- HasFDerivWithinAt.const_cpowproof · cited by 1
- HasFDerivAt.const_cpowproof · cited by 1
- HasStrictFDerivAt.const_cpowproof · cited by 0
- HasStrictDerivAt.const_cpowproof · cited by 0