Mathlib v3 is deprecated. Go to Mathlib v4

Theorem irrational.eventually_forall_le_dist_cast_div_of_denom_le

Modification history

2021-10-23 14:30
src/topology/instances/irrational.lean
feat(topology/instances/irrational): new file (#9872) …
Added irrational.eventually_forall_le_dist_cast_div_of_denom_leView on Github →