Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-08-15 18:18 fa68342d

View on Github →

feat(data/rat): move lemmas to right file, add nat cast lemmas, remove (#1333) redundant lemma

Estimated changes

Modified src/data/rat/basic.lean

added theorem rat.of_int_eq_mk

Modified src/data/rat/cast.lean

added theorem rat.coe_int_eq_mk

added theorem rat.coe_int_eq_of_int

added theorem rat.coe_nat_eq_mk

added theorem rat.mk_eq_div

Modified src/data/rat/floor.lean

Modified src/data/rat/order.lean

deleted theorem rat.coe_int_eq_mk

deleted theorem rat.coe_int_eq_of_int

deleted theorem rat.mk_eq_div

deleted theorem rat.mk_le

deleted theorem rat.of_int_eq_mk