Theorems · Theorem · real analysis
HasDerivAt.div_const
∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {𝕜' : Type u_2} [inst_1 : NormedDivisionRing 𝕜']
[inst_2 : NormedAlgebra 𝕜 𝕜'] {c : 𝕜 → 𝕜'} {c' : 𝕜'},
HasDerivAt c c' x → ∀ (d : 𝕜'), HasDerivAt (fun x => c x / d) (c' / d) x- Defined in
- Mathlib.Analysis.Calculus.Deriv.Mul
- Cited by
- 18 results in Mathlib
- Foundations
- Depth 186 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- NontriviallyNormedFieldstatement and proof · cited by 8,742
- NormedAlgebrastatement and proof · cited by 1,165
- div_eq_mul_invproof · cited by 715
- HasDerivAtstatement and proof · cited by 493
- NormedDivisionRingstatement and proof · cited by 360
- HasDerivAt.congr_simpproof · cited by 82
- HasDerivAt.mul_constproof · cited by 8
Cited by18
Results whose statement or proof uses this declaration.
- DifferentiableAt.div_constproof · cited by 9
- intervalIntegral.intervalIntegrable_rpow'proof · cited by 6
- Real.abs_log_sub_add_sum_range_leproof · cited by 4
- hasDerivAt_ofReal_cpow_const'proof · cited by 2
- integral_Ioi_rpow_of_ltproof · cited by 2
- Real.hasDerivAt_half_log_one_add_div_one_sub_sub_sum_rangeproof · cited by 2
- circleIntegral.integral_sub_zpow_of_neproof · cited by 2
- integral_exp_mul_complexproof · cited by 2
- exp_neg_integrableOn_Ioiproof · cited by 2
- integral_mul_cpow_one_add_sqproof · cited by 1
- integrableOn_add_rpow_Ioi_of_ltproof · cited by 1
- integral_cos_mul_complexproof · cited by 1