Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-08-26 14:50 914c572e

View on Github →

feat(data/rat): add lt, le, and eq def lemmas, move casts into rat to basic (#1348)

Estimated changes

Modified src/data/padics/padic_norm.lean

Modified src/data/padics/padic_numbers.lean

Modified src/data/rat/basic.lean

added theorem rat.coe_int_denom

added theorem rat.coe_int_eq_mk

added theorem rat.coe_int_eq_of_int

added theorem rat.coe_int_num

added theorem rat.coe_int_num_of_denom_eq_one

added theorem rat.coe_nat_denom

added theorem rat.coe_nat_eq_mk

added theorem rat.coe_nat_num

added theorem rat.eq_iff_mul_eq_mul

added theorem rat.inv_def'

added theorem rat.mk_eq_div

added theorem rat.mul_own_denom_eq_num

modified theorem rat.num_denom'

modified theorem rat.num_denom

modified theorem rat.of_int_eq_mk

Modified src/data/rat/cast.lean

deleted theorem rat.coe_int_denom

deleted theorem rat.coe_int_eq_mk

deleted theorem rat.coe_int_eq_of_int

deleted theorem rat.coe_int_num

deleted theorem rat.coe_int_num_of_denom_eq_one

deleted theorem rat.coe_nat_denom

deleted theorem rat.coe_nat_eq_mk

deleted theorem rat.coe_nat_num

deleted theorem rat.mk_eq_div

Modified src/data/rat/order.lean

added theorem rat.div_lt_div_iff_mul_lt_mul

added theorem rat.lt_one_iff_num_lt_denom