Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-08-01 17:01 766807f6

View on Github →

feat(data/rat): refactor into smaller files and add documentation (#1284)

Estimated changes

deleted theorem rat.abs_def
deleted theorem rat.cast_abs
deleted theorem rat.cast_add
deleted theorem rat.cast_add_of_ne_zero
deleted theorem rat.cast_bit0
deleted theorem rat.cast_bit1
deleted theorem rat.cast_coe_int
deleted theorem rat.cast_coe_nat
deleted theorem rat.cast_div
deleted theorem rat.cast_div_of_ne_zero
deleted theorem rat.cast_eq_zero
deleted theorem rat.cast_id
deleted theorem rat.cast_inj
deleted theorem rat.cast_injective
deleted theorem rat.cast_inv
deleted theorem rat.cast_inv_of_ne_zero
deleted theorem rat.cast_le
deleted theorem rat.cast_lt
deleted theorem rat.cast_lt_zero
deleted theorem rat.cast_max
deleted theorem rat.cast_min
deleted theorem rat.cast_mk
deleted theorem rat.cast_mk_of_ne_zero
deleted theorem rat.cast_mul
deleted theorem rat.cast_mul_of_ne_zero
deleted theorem rat.cast_ne_zero
deleted theorem rat.cast_neg
deleted theorem rat.cast_nonneg
deleted theorem rat.cast_nonpos
deleted theorem rat.cast_of_int
deleted theorem rat.cast_one
deleted theorem rat.cast_pos
deleted theorem rat.cast_pow
deleted theorem rat.cast_sub
deleted theorem rat.cast_sub_of_ne_zero
deleted theorem rat.cast_zero
deleted def rat.ceil
deleted theorem rat.ceil_add_int
deleted theorem rat.ceil_coe
deleted theorem rat.ceil_le
deleted theorem rat.ceil_mono
deleted theorem rat.ceil_sub_int
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_nat_denom
deleted theorem rat.coe_nat_num
deleted theorem rat.eq_cast
deleted theorem rat.eq_cast_of_ne_zero
deleted theorem rat.exists_mul_self
deleted def rat.floor
deleted theorem rat.floor_add_int
deleted theorem rat.floor_coe
deleted theorem rat.floor_le
deleted theorem rat.floor_lt
deleted theorem rat.floor_mono
deleted theorem rat.floor_sub_int
deleted theorem rat.le_ceil
deleted theorem rat.le_floor
deleted theorem rat.le_nat_ceil
deleted theorem rat.lt_nat_ceil
deleted theorem rat.lt_succ_floor
deleted theorem rat.mk_eq_div
deleted theorem rat.mk_le
deleted theorem rat.mk_nonneg
deleted theorem rat.mul_cast_comm
deleted def rat.nat_ceil
deleted theorem rat.nat_ceil_add_nat
deleted theorem rat.nat_ceil_coe
deleted theorem rat.nat_ceil_le
deleted theorem rat.nat_ceil_lt_add_one
deleted theorem rat.nat_ceil_mono
deleted theorem rat.nat_ceil_zero
deleted theorem rat.nonneg_iff_zero_le
deleted theorem rat.num_pos_iff_pos
deleted theorem rat.of_int_eq_mk
deleted def rat.sqrt
deleted theorem rat.sqrt_eq
deleted theorem rat.sqrt_nonneg
added theorem rat.cast_abs
added theorem rat.cast_add
added theorem rat.cast_bit0
added theorem rat.cast_bit1
added theorem rat.cast_coe_int
added theorem rat.cast_coe_nat
added theorem rat.cast_div
added theorem rat.cast_eq_zero
added theorem rat.cast_id
added theorem rat.cast_inj
added theorem rat.cast_injective
added theorem rat.cast_inv
added theorem rat.cast_le
added theorem rat.cast_lt
added theorem rat.cast_lt_zero
added theorem rat.cast_max
added theorem rat.cast_min
added theorem rat.cast_mk
added theorem rat.cast_mk_of_ne_zero
added theorem rat.cast_mul
added theorem rat.cast_ne_zero
added theorem rat.cast_neg
added theorem rat.cast_nonneg
added theorem rat.cast_nonpos
added theorem rat.cast_of_int
added theorem rat.cast_one
added theorem rat.cast_pos
added theorem rat.cast_pow
added theorem rat.cast_sub
added theorem rat.cast_zero
added theorem rat.coe_int_denom
added theorem rat.coe_int_num
added theorem rat.coe_nat_denom
added theorem rat.coe_nat_num
added theorem rat.eq_cast
added theorem rat.eq_cast_of_ne_zero
added theorem rat.mul_cast_comm
added def rat.ceil
added theorem rat.ceil_add_int
added theorem rat.ceil_coe
added theorem rat.ceil_le
added theorem rat.ceil_mono
added theorem rat.ceil_sub_int
added def rat.floor
added theorem rat.floor_add_int
added theorem rat.floor_coe
added theorem rat.floor_def
added theorem rat.floor_le
added theorem rat.floor_lt
added theorem rat.floor_mono
added theorem rat.floor_sub_int
added theorem rat.le_ceil
added theorem rat.le_floor
added theorem rat.le_nat_ceil
added theorem rat.lt_nat_ceil
added theorem rat.lt_succ_floor
added def rat.nat_ceil
added theorem rat.nat_ceil_add_nat
added theorem rat.nat_ceil_coe
added theorem rat.nat_ceil_le
added theorem rat.nat_ceil_mono
added theorem rat.nat_ceil_zero
added theorem rat.abs_def
added theorem rat.coe_int_eq_mk
added theorem rat.coe_int_eq_of_int
added theorem rat.exists_mul_self
added theorem rat.mk_eq_div
added theorem rat.mk_le
added theorem rat.mk_nonneg
added theorem rat.nonneg_iff_zero_le
added theorem rat.num_pos_iff_pos
added theorem rat.of_int_eq_mk
added def rat.sqrt
added theorem rat.sqrt_eq
added theorem rat.sqrt_nonneg