Mathlib v3 is deprecated. Go to Mathlib v4

Theorem exists_rat_btwn

Modification history

2018-01-26 02:52

algebra/archimedean.lean

feat(algebra/archimedean): generalize real thms to archimedean fields

Added exists_rat_btwn View on Github →

2018-01-19 17:05

analysis/real.lean

feat(analysis/real): swap out the definition of real, shorten proofs

Deleted exists_rat_btwn View on Github →

2017-10-25 21:55

analysis/real.lean

refactor(analysis/real): use more coe instead of of_rat

Added exists_rat_btwn View on Github →