Theorems · Theorem · special functions
Complex.Gamma_eq_integral
∀ {s : ℂ}, 0 < s.re → Complex.Gamma s = s.GammaIntegral- Cited by
- 6 results in Mathlib
- Foundations
- Depth 280 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.
- Realstatement and proof · cited by 25,697
- Complexstatement and proof · cited by 5,565
- Nat.cast_zeroproof · cited by 1,870
- Complex.restatement and proof · cited by 882
- lt_of_not_geproof · cited by 374
- Complex.Gammastatement · cited by 96
- Complex.GammaIntegralstatement · cited by 12
Cited by6
Results whose statement or proof uses this declaration.
- Complex.Gamma_oneproof · cited by 9
- Complex.differentiableAt_Gammaproof · cited by 8
- Real.Gamma_eq_integralproof · cited by 4
- Complex.integral_cpow_mul_exp_neg_mul_Ioiproof · cited by 2
- Complex.Gamma_mul_Gamma_eq_betaIntegralproof · cited by 1
- Complex.approx_Gamma_integral_tendsto_Gamma_integralproof · cited by 1