factorial-positive

Leighton Leandro Estrada Rayme

0.1 Factorial

Definition 1 Factorial
✓
#

Lean declarations

For any natural number \(n\), we define the factorial of \(n\), denoted by \(n!\), recursively as:

  • \(0! = 1\)

  • \((n+1)! = (n+1) \cdot n!\)

Theorem 2 Positivity of Factorials
✓
#

Uses

Lean declarations

For every natural number \(n\), the factorial of \(n\) is strictly positive:

\[ n! {\gt} 0 \]
Proof ▶

By induction on \(n\).

  • Base case: \(0! = 1 {\gt} 0\).

  • Inductive step: Assume \(n! {\gt} 0\). Then \((n+1)! = (n+1) \cdot n!\). Since \(n+1 {\gt} 0\) and \(n! {\gt} 0\) (by inductive hypothesis), their product is positive.