Mathlib v3 is deprecated. Go to Mathlib v4

Theorem eventually_residual_irrational

Modification history

2021-10-23 14:30
src/number_theory/liouville/residual.lean
feat(topology/instances/irrational): new file (#9872) …
Modified eventually_residual_irrationalView on Github →
2021-10-11 07:59
src/number_theory/liouville/residual.lean
feat(number_theory/liouville): Liouville numbers form a dense Gδ set (#9646)
Added eventually_residual_irrationalView on Github →