OAI/NumberTheory/Ostmann/Conclusion/BadFraction.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.Conclusion.log_factorial_lower line 8
2. theorem OAI.Ostmann.Conclusion.log_factorial_upper line 19
3. theorem OAI.Ostmann.Conclusion.factorial_ratio_bound line 25
4. theorem OAI.Ostmann.Conclusion.badArrangement_fraction_bound line 39