Theorems · Theorem · number theory
Nat.factorial_pos
∀ (n : ℕ), 0 < n.factorial
- Defined in
- Mathlib.Data.Nat.Factorial.Basic
- Cited by
- 99 results in Mathlib
- Foundations
- Depth 13 from the axioms, rests on 61 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Nat.factorialstatement · cited by 616
Cited by99
Results whose statement or proof uses this declaration.
- Nat.factorial_ne_zeroproof · cited by 56
- Nat.descFactorial_eq_factorial_mul_chooseproof · cited by 12
- Nat.factorial_leproof · cited by 10
- Nat.choose_eq_factorial_div_factorialproof · cited by 8
- Nat.self_le_factorialproof · cited by 7
- Nat.exists_infinite_primesproof · cited by 7
- AnalyticAt.hasFPowerSeriesAtproof · cited by 7
- Complex.exp_boundproof · cited by 6
- Nat.cast_chooseproof · cited by 6
- Real.sum_le_exp_of_nonnegproof · cited by 5
- Stirling.log_stirlingSeq_sdiff_hasSumproof · cited by 4
- Polynomial.natDegree_preHilbertPolyproof · cited by 3