Commit 2021-06-21 03:37 3925fc0f
View on Github →feat(analysis/liouville/liouville_constant.lean): create a file and introduce Liouville's constant (#7996) Introduce a new file and the definition of Liouville's number. This is on the way to PR #4301.