Theorems · Theorem · special functions
Complex.Gamma_add_one
∀ (s : ℂ), s ≠ 0 → Complex.Gamma (s + 1) = s * Complex.Gamma s
The recurrence relation for the Γ function.
- Cited by
- 12 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.
Cites16
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realproof · cited by 25,697
- Complexstatement and proof · cited by 5,565
- one_mulproof · cited by 2,841
- Nat.cast_oneproof · cited by 2,501
- Nat.cast_zeroproof · cited by 1,870
- one_ne_zeroproof · cited by 885
- Complex.reproof · cited by 882
- div_oneproof · cited by 629
- lt_of_not_geproof · cited by 374
- neg_neg_of_posproof · cited by 227
- Nat.floorproof · cited by 215
- Complex.Gammastatement and proof · cited by 96
Cited by12
Results whose statement or proof uses this declaration.
- Real.Gamma_add_oneproof · cited by 13
- Complex.Gamma_nat_eq_factorialproof · cited by 4
- Complex.Gamma_neg_nat_eq_zeroproof · cited by 4
- Complex.tendsto_self_mul_Gamma_nhds_zeroproof · cited by 2
- Complex.GammaSeq_tendsto_Gammaproof · cited by 2
- riemannZeta_eq_mul_completedRiemannZeta₀proof · cited by 1
- Complex.Gammaℂ_add_oneproof · cited by 1
- Complex.Gammaℝ_add_twoproof · cited by 1
- Complex.deriv_Gamma_add_oneproof · cited by 1
- Complex.one_div_Gamma_eq_self_mul_one_div_Gamma_add_oneproof · cited by 1
- Complex.not_continuousAt_Gamma_neg_natproof · cited by 1
- Complex.digamma_apply_add_oneproof · cited by 0