liouville_constant.lean): create a file and introduce Liouville's constant (#7996)

Commit

4 years ago

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.

Author

adomani

Parents

4d69b0f4

mathlib 3925fc0f - feat(analysis/liouville/liouville_constant.lean): create a file and introduce Liouville's constant (#7996)

mathlib
3925fc0f - feat(analysis/liouville/liouville_constant.lean): create a file and introduce Liouville's constant (#7996)