Factorial estimates

Elementary bounds comparing factorials and powers.

Main results

• Nat.pow_self_le_three_pow_mul_factorial: n ^ n ≤ 3 ^ n * n!.

theorem Nat.pow_self_le_three_pow_mul_factorial (n : ℕ) : n ^ n ≤ 3 ^ n * n.factorial

Elementary factorial estimate: n ^ n ≤ 3 ^ n * n!, from n ^ n / n! ≤ exp n and e < 3.