Theorems · Theorem · number theory
HurwitzZeta.differentiableAt_hurwitzZetaEven_sub_one_div
∀ (a : UnitAddCircle), DifferentiableAt ℂ (fun s => HurwitzZeta.hurwitzZetaEven a s - 1 / (s - 1) / s.Gammaℝ) 1
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 302 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites29
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Complexstatement and proof · cited by 5,565
- add_zeroproof · cited by 2,707
- Filter.univ_mem'proof · cited by 1,672
- Filter.mp_memproof · cited by 1,537
- one_ne_zeroproof · cited by 885
- add_assocproof · cited by 746
- div_eq_mul_invproof · cited by 715
- DifferentiableAtstatement and proof · cited by 617
- neg_subproof · cited by 272
- neg_add_cancelproof · cited by 256
- Function.update_of_neproof · cited by 198
- UnitAddCirclestatement and proof · cited by 157
Cited by3
Results whose statement or proof uses this declaration.
- HurwitzZeta.tendsto_hurwitzZetaEven_sub_one_div_nhds_oneproof · cited by 2
- HurwitzZeta.differentiableAt_hurwitzZeta_sub_one_divproof · cited by 1
- HurwitzZeta.differentiable_hurwitzZetaEven_sub_hurwitzZetaEvenproof · cited by 1