mathlib3

2f566202 - feat(data/real/irrational): define Liouville numbers (#6158)

feat(data/real/irrational): define Liouville numbers (#6158) Prove that a Liouville number is irrational Co-authored-by: Jujian Zhang <jujian.zhang1998@outlook.com>