Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-21 05:20 60af3bda

View on Github →

feat(data/rat/denumerable): Make mk_rat into a simp lemma (#12821)

Estimated changes

modified theorem cardinal.mk_rat