mathlib3
36b35107 - feat(data/nat/factorial): additional inequalities (#6026)

Commit
4 years ago
feat(data/nat/factorial): additional inequalities (#6026) I added two lemmas about factorials. I use them in the Liouville PR #4301.
Author
Parents
Loading