Theorems · Theorem · real analysis
deriv_norm_ofReal_cpow
∀ (c : ℂ) {t : ℝ}, 0 < t → deriv (fun x => ‖↑x ^ c‖) t = c.re * t ^ (c.re - 1)- Cited by
- 1 results in Mathlib
- Foundations
- Depth 209 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.
- Realstatement and proof · cited by 25,697
- Complexstatement and proof · cited by 5,565
- Norm.normstatement · cited by 5,413
- Filter.univ_mem'proof · cited by 1,672
- Complex.ofRealstatement · cited by 1,654
- Filter.mp_memproof · cited by 1,537
- Complex.restatement and proof · cited by 882
- derivstatement · cited by 676
- Complex.norm_cpow_eq_rpow_re_of_posproof · cited by 21
- Filter.EventuallyEq.deriv_eqproof · cited by 14
- eventually_gt_nhdsproof · cited by 8
- Real.deriv_rpow_constproof · cited by 5
Cited by1
Results whose statement or proof uses this declaration.
- integrableOn_Ioi_deriv_norm_ofReal_cpowproof · cited by 0