Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-10 11:15 e52108d7

View on Github →

chore(data/int/basic): move content requiring advanced imports (#3334) data.int.basic had grown to require substantial imports from algebra.*. This PR moves out the end of this file into separate files. As a consequence it's then possible to separate out data.multiset.basic into some further pieces.

Estimated changes

deleted theorem add_monoid_hom.ext_int
deleted theorem int.cast_abs
deleted theorem int.cast_add
deleted def int.cast_add_hom
deleted theorem int.cast_bit0
deleted theorem int.cast_bit1
deleted theorem int.cast_coe_nat'
deleted theorem int.cast_coe_nat
deleted theorem int.cast_commute
deleted theorem int.cast_eq_zero
deleted theorem int.cast_id
deleted theorem int.cast_inj
deleted theorem int.cast_injective
deleted theorem int.cast_le
deleted theorem int.cast_lt
deleted theorem int.cast_lt_zero
deleted theorem int.cast_max
deleted theorem int.cast_min
deleted theorem int.cast_mul
deleted theorem int.cast_ne_zero
deleted theorem int.cast_neg
deleted theorem int.cast_neg_of_nat
deleted theorem int.cast_neg_succ_of_nat
deleted theorem int.cast_nonneg
deleted theorem int.cast_nonpos
deleted theorem int.cast_of_nat
deleted theorem int.cast_one
deleted theorem int.cast_pos
deleted def int.cast_ring_hom
deleted theorem int.cast_sub
deleted theorem int.cast_sub_nat_nat
deleted theorem int.cast_two
deleted theorem int.cast_zero
deleted theorem int.coe_cast_add_hom
deleted theorem int.coe_cast_ring_hom
deleted theorem int.coe_nat_bit0
deleted theorem int.coe_nat_bit1
deleted theorem int.commute_cast
deleted theorem int.mem_range_iff
deleted theorem int.nat_cast_eq_coe_nat
deleted def int.of_nat_hom
deleted def int.range
deleted theorem ring_hom.eq_int_cast'
deleted theorem ring_hom.eq_int_cast
deleted theorem ring_hom.ext_int
deleted theorem ring_hom.map_int_cast
added theorem add_monoid_hom.ext_int
added theorem int.cast_abs
added theorem int.cast_add
added def int.cast_add_hom
added theorem int.cast_bit0
added theorem int.cast_bit1
added theorem int.cast_coe_nat'
added theorem int.cast_coe_nat
added theorem int.cast_commute
added theorem int.cast_id
added theorem int.cast_le
added theorem int.cast_lt
added theorem int.cast_lt_zero
added theorem int.cast_max
added theorem int.cast_min
added theorem int.cast_mul
added theorem int.cast_neg
added theorem int.cast_neg_of_nat
added theorem int.cast_nonneg
added theorem int.cast_nonpos
added theorem int.cast_of_nat
added theorem int.cast_one
added theorem int.cast_pos
added theorem int.cast_sub
added theorem int.cast_sub_nat_nat
added theorem int.cast_two
added theorem int.cast_zero
added theorem int.coe_cast_add_hom
added theorem int.coe_cast_ring_hom
added theorem int.coe_nat_bit0
added theorem int.coe_nat_bit1
added theorem int.commute_cast
added def int.of_nat_hom
added theorem ring_hom.eq_int_cast'
added theorem ring_hom.eq_int_cast
added theorem ring_hom.ext_int
added theorem ring_hom.map_int_cast
added theorem int.cast_eq_zero
added theorem int.cast_inj
added theorem int.cast_injective
added theorem int.cast_ne_zero
added theorem int.mem_range_iff
added def int.range
deleted theorem multiset.card_range
deleted theorem multiset.mem_range
deleted def multiset.range
deleted theorem multiset.range_subset
deleted theorem multiset.range_succ
deleted theorem multiset.range_zero
added theorem multiset.card_range
added theorem multiset.mem_range
added def multiset.range
added theorem multiset.range_subset
added theorem multiset.range_succ
added theorem multiset.range_zero
modified theorem rat.coe_int_inj