mathlib
60af3bda - feat(data/rat/denumerable): Make `mk_rat` into a simp lemma (#12821)

Commit

3 years ago

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

Author

vihdzp

vihdzp

Parents

Loading