Theorem cardinal.mk_rat
Modification history
2022-06-05 07:36
src/data/rat/denumerable.lean
refactor(set_theory/*): change `omega` to `aleph_0` + golf (#14467) …
Modified cardinal.mk_ratView on Github →2022-03-21 05:20
src/data/rat/denumerable.lean
feat(data/rat/denumerable): Make `mk_rat` into a simp lemma (#12821)
Modified cardinal.mk_ratView on Github →2021-10-04 19:37
src/data/rat/denumerable.lean
feat(set_theory/cardinal,*): assorted lemmas (#9516) …
Modified cardinal.mk_ratView on Github →