Mathlib v3 is deprecated. Go to Mathlib v4

Theorem exists_nat_one_div_lt

Modification history

2019-09-27 07:02
src/algebra/archimedean.lean
chore(*): drop some unused args reported by `#sanity_check_mathlib` (#1490) …
Modified exists_nat_one_div_ltView on Github →
2018-10-02 14:08
algebra/archimedean.lean
feat(data/real/cau_seq): relate cauchy sequence completeness and filter completeness
Added exists_nat_one_div_ltView on Github →