Commit 2019-06-15 01:30 3ad35223
View on Github →feat(data/rat/denumerable): computable denumerability of Q (#1104)
- feat(data/rat/denumerable): computable denumerability of Q
- blah
- fix build
- remove unnecessary decidable_eq
- add header
- delete rat.lean and update imports
- fix build
- prove exists_not_mem_finset
- massively speed up encode
- minor change