Mathlib Map

Theorems · Theorem · special functions

Complex.betaIntegral_eq_Gamma_mul_div

∀ (u v : ℂ), 0 < u.re → 0 < v.re → u.betaIntegral v = Complex.Gamma u * Complex.Gamma v / Complex.Gamma (u + v)
Defined in
Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Cited by
1 results in Mathlib
Foundations
Depth 286 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.

ProbabilityTheory.beta_eq_betaIntegralReal · cited by 1ProbabilityTheory.beta_eq…Real · cited by 25697RealComplex · cited by 5565ComplexComplex.re · cited by 882Complex.remul_div_cancel_left₀ · cited by 111mul_div_cancel_left₀Complex.Gamma · cited by 96Complex.Gammaadd_pos · cited by 28add_posComplex.betaIntegral · cited by 9Complex.betaIntegralComplex.Gamma_ne_zero_of_re_pos · cited by 2Complex.Gamma_ne_zero_of_…Complex.Gamma_mul_Gamma_eq_betaIntegral · cited by 1Complex.Gamma_mul_Gamma_e…Complex.betaIntegral_eq_Gamma…CITED BYCITES

Cites9

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

Cited by1

Results whose statement or proof uses this declaration.