Theorems · Theorem · real analysis
hasDerivAt_const
∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
[inst_2 : NormedSpace 𝕜 F] (x : 𝕜) (c : F), HasDerivAt (fun x => c) 0 x- Defined in
- Mathlib.Analysis.Calculus.Deriv.Basic
- Cited by
- 15 results in Mathlib
- Foundations
- Depth 167 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.
- NormedAddCommGroupstatement and proof · cited by 15,752
- NormedSpacestatement and proof · cited by 12,499
- NontriviallyNormedFieldstatement and proof · cited by 8,742
- nhdsproof · cited by 5,554
- SProd.sprodproof · cited by 1,750
- HasDerivAtstatement · cited by 493
- hasDerivAtFilter_constproof · cited by 8
Cited by15
Results whose statement or proof uses this declaration.
- deriv_constproof · cited by 11
- InformationTheory.hasDerivAt_klFunproof · cited by 3
- hasDerivAt_integral_of_dominated_loc_of_lipproof · cited by 2
- QuadraticMap.hasLineDerivAtproof · cited by 2
- expNegInvGlue.hasDerivAt_polynomial_eval_inv_mulproof · cited by 2
- HasFDerivWithinAt.hasLineDerivWithinAtproof · cited by 2
- norm_image_sub_le_of_norm_deriv_right_le_segmentproof · cited by 2
- Real.hasDerivAt_Gamma_one_halfproof · cited by 1
- integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable_aux1proof · cited by 1
- hasDerivAt_natCastproof · cited by 0
- hasDerivAt_ofNatproof · cited by 0
- hasDerivAt_oneproof · cited by 0