Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-07-30 00:48 bce43b3c

View on Github →

feat(data/rat): new rat representation using canonical elements This yields better performance in long rational computations provided the numbers can be simplified.

Estimated changes

added theorem int.coe_nat_dvd_left
added theorem int.coe_nat_dvd_right
added theorem int.div_sign
added theorem int.nat_abs_add_le
added theorem int.nat_abs_mul
added theorem int.nat_abs_neg_of_nat
added theorem int.neg_nat_succ
added theorem int.neg_pred
added theorem int.neg_succ
added def int.pred
added theorem int.pred_nat_succ
added theorem int.pred_neg_pred
added theorem int.pred_succ
added theorem int.sign_mul
added def int.succ
added theorem int.succ_neg_nat_succ
added theorem int.succ_neg_succ
added theorem int.succ_pred
deleted theorem nat.comprime_one_left
deleted theorem nat.comprime_one_right
added theorem nat.coprime_one_left
added theorem nat.coprime_one_right
modified theorem linear_order_cases_on_eq
modified theorem linear_order_cases_on_gt
modified theorem linear_order_cases_on_lt
deleted theorem not_antimono
added theorem rat.add_def
added def rat.ceil
added def rat.floor
added theorem rat.inv_def
added theorem rat.lift_binop_eq
added def rat.mk
added theorem rat.mk_eq
added theorem rat.mk_eq_zero
added def rat.mk_nat
added theorem rat.mk_nat_eq
added theorem rat.mk_nonneg
added def rat.mk_pnat
added theorem rat.mk_pnat_eq
added theorem rat.mk_zero
added theorem rat.mul_def
added theorem rat.neg_def
added theorem rat.nonneg_iff_zero_le
added theorem rat.num_denom'
added theorem rat.num_denom
added def rat.of_int
added theorem rat.zero_mk
added theorem rat.zero_mk_nat
added theorem rat.zero_mk_pnat
added theorem rat.{u}
added structure rat
deleted def rat
modified theorem mem_image