Commit 2021-06-23 11:50 d9eed422

feat(analysis/liouville/inequalities_and_series): two useful inequalities for Liouville (#8001) This PR creates a file with proves two very specific inequalities. They will be useful for the Liouville PR, showing that transcendental Liouville numbers exist. After the initial code review, I scattered an initial segment of this PR into mathlib. What is left might only be useful in the context of proving the transcendence of Liouville's constants. Given the shortness of this file, I may move it into the main liouville_constant, after PR #8020 is merged.