Theorems · Theorem · special functions
Complex.Gamma_mul_Gamma_one_sub
∀ (z : ℂ), Complex.Gamma z * Complex.Gamma (1 - z) = ↑Real.pi / Complex.sin (↑Real.pi * z)
Euler's reflection formula for the complex Gamma function.
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 283 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites55
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpaceproof · cited by 24,529
- Filterproof · cited by 8,121
- Complexstatement and proof · cited by 5,565
- nhdsproof · cited by 5,554
- Filter.Tendstoproof · cited by 3,814
- one_mulproof · cited by 2,841
- Nat.cast_oneproof · cited by 2,501
- Filter.atTopproof · cited by 2,405
- Finset.prodproof · cited by 2,356
- mul_commproof · cited by 2,262
- MulZeroClass.mul_zeroproof · cited by 2,091
- Real.pistatement and proof · cited by 1,774
Cited by3
Results whose statement or proof uses this declaration.
- Complex.Gamma_ne_zeroproof · cited by 6
- Complex.Gammaℝ_one_sub_mul_Gammaℝ_one_addproof · cited by 1
- Real.Gamma_mul_Gamma_one_subproof · cited by 0