Theorems · Theorem · special functions
Real.BohrMollerup.f_nat_eq
∀ {f : ℝ → ℝ} {n : ℕ},
(∀ {y : ℝ}, 0 < y → f (y + 1) = f y + Real.log y) → n ≠ 0 → f ↑n = f 1 + Real.log ↑(n - 1).factorial- Cited by
- 2 results in Mathlib
- Foundations
- Depth 173 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites18
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
- add_zeroproof · cited by 2,707
- Nat.cast_oneproof · cited by 2,501
- mul_commproof · cited by 2,262
- LT.lt.ne'proof · cited by 1,417
- Real.logstatement and proof · cited by 939
- add_assocproof · cited by 746
- Nat.factorialstatement and proof · cited by 616
- Nat.cast_addproof · cited by 586
- Nat.cast_mulproof · cited by 309
- tsub_selfproof · cited by 154
- Nat.cast_ne_zeroproof · cited by 113
Cited by2
Results whose statement or proof uses this declaration.
- Real.BohrMollerup.ge_logGammaSeqproof · cited by 1
- Real.BohrMollerup.le_logGammaSeqproof · cited by 1