A logarithmic lower bound for the factorial

Bounding one term of the exponential series gives n log n - n ≤ log (n!), including at zero.

theorem Nat.mul_log_sub_le_log_factorial (n : ℕ) : ↑n * Real.log ↑n - ↑n ≤ Real.log ↑n.factorial

The logarithm of the factorial is at least n log n - n.