Theorems · Theorem · special functions
Real.hasDerivAt_Gamma_nat
∀ (n : ℕ), HasDerivAt Real.Gamma (↑n.factorial * (-Real.eulerMascheroniConstant + ↑(harmonic n))) (↑n + 1)
- Defined in
- Mathlib.NumberTheory.Harmonic.GammaDeriv
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 289 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
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
- Nat.cast_oneproof · cited by 2,501
- Nat.cast_zeroproof · cited by 1,870
- Nat.factorialstatement · cited by 616
- HasDerivAtstatement · cited by 493
- neg_neg_of_posproof · cited by 227
- sub_eq_zero_of_eqproof · cited by 154
- DifferentiableAt.hasDerivAtproof · cited by 114
- Real.Gammastatement · cited by 76
- Real.eulerMascheroniConstantstatement · cited by 41
- harmonicstatement · cited by 27
- Real.differentiableAt_Gammaproof · cited by 5
Cited by2
Results whose statement or proof uses this declaration.
- Complex.hasDerivAt_Gamma_natproof · cited by 2
- Real.hasDerivAt_Gamma_oneproof · cited by 1