Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-08 05:22 ad7038e5

View on Github →

refactor(*): supremum of refactoring PRs #17384 #17398 #17406 #17407 #17408 (#17405) This is going to be another combination PR. If at any point every constituent PR has been delegated, and I have a green check here, I will hand it to bors (i.e. without waiting for an explicit approval of this PR). The only difference relative to the constituent PRs are any further import adjustments required to keep everything working together. Using this PR means I can locally build everything together to check for interactions. Depends on

Estimated changes

deleted theorem field.to_is_field
deleted theorem is_field.nontrivial
deleted structure is_field
deleted def qsmul_rec
deleted theorem rat.cast_def
deleted theorem rat.cast_mk'
deleted def rat.cast_rec
deleted theorem rat.smul_def
deleted theorem semifield.to_is_field
deleted theorem uniq_inv_of_is_field
added theorem field.to_is_field
added theorem is_field.nontrivial
added structure is_field
added def qsmul_rec
added theorem rat.cast_def
added theorem rat.cast_mk'
added def rat.cast_rec
added theorem rat.smul_def
added theorem semifield.to_is_field
added theorem uniq_inv_of_is_field
deleted theorem add_mul_self_eq
deleted theorem add_one_mul
deleted theorem bit0_eq_two_mul
deleted theorem boole_mul
deleted theorem distrib_three_right
deleted theorem ite_and_mul_zero
deleted theorem ite_mul
deleted theorem ite_mul_zero_left
deleted theorem ite_mul_zero_right
deleted theorem left_distrib
deleted theorem mul_add_one
deleted theorem mul_boole
deleted theorem mul_ite
deleted theorem mul_neg
deleted theorem mul_neg_one
deleted theorem mul_one_add
deleted theorem mul_two
deleted theorem neg_eq_neg_one_mul
deleted theorem neg_mul
deleted theorem neg_mul_comm
deleted theorem neg_mul_eq_mul_neg
deleted theorem neg_mul_eq_neg_mul
deleted theorem neg_mul_neg
deleted theorem neg_one_mul
deleted theorem one_add_mul
deleted theorem one_add_one_eq_two
deleted theorem right_distrib
deleted theorem two_mul
added theorem add_mul_self_eq
added theorem add_one_mul
added theorem bit0_eq_two_mul
added theorem boole_mul
added theorem distrib_three_right
added theorem ite_and_mul_zero
added theorem ite_mul
added theorem ite_mul_zero_left
added theorem ite_mul_zero_right
added theorem left_distrib
added theorem mul_add_one
added theorem mul_boole
added theorem mul_ite
added theorem mul_neg
added theorem mul_neg_one
added theorem mul_one_add
added theorem mul_two
added theorem neg_eq_neg_one_mul
added theorem neg_mul
added theorem neg_mul_comm
added theorem neg_mul_eq_mul_neg
added theorem neg_mul_eq_neg_mul
added theorem neg_mul_neg
added theorem neg_one_mul
added theorem one_add_mul
added theorem one_add_one_eq_two
added theorem right_distrib
added theorem two_mul
added theorem int.cast_add
added theorem int.cast_bit0
added theorem int.cast_bit1
added theorem int.cast_coe_nat
added theorem int.cast_four
added theorem int.cast_neg
added theorem int.cast_neg_of_nat
added theorem int.cast_one
added theorem int.cast_sub
added theorem int.cast_sub_nat_nat
added theorem int.cast_three
added theorem int.cast_two
added theorem int.cast_zero
added theorem int.coe_nat_bit0
added theorem int.coe_nat_bit1
added theorem int.neg_of_nat_eq
added theorem nat.cast_pred
added theorem nat.cast_sub
deleted theorem int.cast_add
deleted theorem int.cast_bit0
deleted theorem int.cast_bit1
deleted theorem int.cast_coe_nat
deleted theorem int.cast_four
deleted theorem int.cast_neg
deleted theorem int.cast_neg_of_nat
deleted theorem int.cast_neg_succ_of_nat
deleted theorem int.cast_one
deleted theorem int.cast_sub
deleted theorem int.cast_sub_nat_nat
deleted theorem int.cast_three
deleted theorem int.cast_two
deleted theorem int.cast_zero
deleted theorem int.coe_nat_bit0
deleted theorem int.coe_nat_bit1
deleted theorem int.neg_of_nat_eq
deleted theorem nat.cast_pred
deleted theorem nat.cast_sub
deleted theorem rat.add_denom_dvd
deleted theorem rat.add_num_denom'
deleted theorem rat.add_num_denom
deleted theorem rat.coe_int_div
deleted theorem rat.coe_int_div_self
deleted theorem rat.coe_nat_div
deleted theorem rat.coe_nat_div_self
deleted theorem rat.coe_pnat_denom
deleted theorem rat.denom_dvd
deleted theorem rat.denom_mk
deleted theorem rat.div_int_inj
deleted theorem rat.ext
deleted theorem rat.ext_iff
deleted theorem rat.inv_coe_int_denom
deleted theorem rat.inv_coe_int_num
deleted theorem rat.inv_coe_nat_denom
deleted theorem rat.inv_coe_nat_num
deleted theorem rat.inv_def'
deleted theorem rat.mk_pnat_denom
deleted theorem rat.mk_pnat_denom_dvd
deleted theorem rat.mk_pnat_num
deleted theorem rat.mk_pnat_pnat_denom_eq
deleted theorem rat.mul_denom
deleted theorem rat.mul_denom_dvd
deleted theorem rat.mul_denom_eq_num
deleted theorem rat.mul_num
deleted theorem rat.mul_num_denom'
deleted theorem rat.mul_self_denom
deleted theorem rat.mul_self_num
deleted theorem rat.num_denom_mk
deleted theorem rat.num_div_eq_of_coprime
deleted theorem rat.num_dvd
deleted theorem rat.num_mk
deleted def rat.pnat_denom
deleted theorem rat.pnat_denom_one
deleted theorem rat.pnat_denom_zero
deleted theorem rat.substr_num_denom'
deleted structure rat
added theorem rat.ext
added theorem rat.ext_iff
added structure rat
added theorem rat.add_denom_dvd
added theorem rat.add_num_denom'
added theorem rat.add_num_denom
added theorem rat.coe_int_div
added theorem rat.coe_int_div_self
added theorem rat.coe_nat_div
added theorem rat.coe_nat_div_self
added theorem rat.coe_pnat_denom
added theorem rat.denom_dvd
added theorem rat.denom_mk
added theorem rat.div_int_inj
added theorem rat.inv_coe_int_denom
added theorem rat.inv_coe_int_num
added theorem rat.inv_coe_nat_denom
added theorem rat.inv_coe_nat_num
added theorem rat.inv_def'
added theorem rat.mk_pnat_denom
added theorem rat.mk_pnat_denom_dvd
added theorem rat.mk_pnat_num
added theorem rat.mul_denom
added theorem rat.mul_denom_dvd
added theorem rat.mul_denom_eq_num
added theorem rat.mul_num
added theorem rat.mul_num_denom'
added theorem rat.mul_self_denom
added theorem rat.mul_self_num
added theorem rat.num_denom_mk
added theorem rat.num_dvd
added theorem rat.num_mk
added def rat.pnat_denom
added theorem rat.pnat_denom_one
added theorem rat.pnat_denom_zero
added theorem rat.substr_num_denom'
added theorem nat.mem_range_succ
deleted theorem set.nat.mem_range_succ