Mathlib Map

Theorems · Definition · special functions

Real.Gamma

ℝ → ℝ

The Γ function (of a real variable s).

Defined in
Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Cited by
76 results in Mathlib
Foundations
Depth 254 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Real.Gamma_pos_of_pos · cited by 17Real.Gamma_pos_of_posReal.Gamma_add_one · cited by 13Real.Gamma_add_oneComplex.Gamma_ofReal · cited by 9Complex.Gamma_ofRealProbabilityTheory.beta · cited by 9ProbabilityTheory.betaReal.Gamma_one · cited by 7Real.Gamma_oneProbabilityTheory.gammaPDFReal · cited by 6ProbabilityTheory.gammaPD…Real.Gamma_one_half_eq · cited by 6Real.Gamma_one_half_eqReal.differentiableAt_Gamma · cited by 5Real.differentiableAt_Gam…Real.convexOn_log_Gamma · cited by 5Real.convexOn_log_GammaReal.doublingGamma · cited by 5Real.doublingGammaReal.Gamma_nat_eq_factorial · cited by 5Real.Gamma_nat_eq_factori…Real.Gamma_eq_integral · cited by 4Real.Gamma_eq_integralintegral_rpow_mul_exp_neg_rpow · cited by 4integral_rpow_mul_exp_neg…Real.integral_rpow_mul_exp_neg_mul_Ioi · cited by 3Real.integral_rpow_mul_ex…Complex.Gamma_one_half_eq · cited by 3Complex.Gamma_one_half_eqReal · cited by 25697RealComplex.ofReal · cited by 1654Complex.ofRealComplex.re · cited by 882Complex.reComplex.Gamma · cited by 96Complex.GammaReal.GammaCITED BYCITES

Cites4

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by79

Results whose statement or proof uses this declaration.