Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-08 20:55 47b51515

View on Github →

refactor(*): supremum of refactoring PRs #17405 #17418 #17419 #17420 #17421 #17422 #17423 #17427 #17430 (#17424)

Estimated changes

deleted theorem dvd.elim
deleted theorem dvd.elim_left
deleted theorem dvd.intro
deleted theorem dvd.intro_left
deleted theorem dvd_and_not_dvd_iff
deleted theorem dvd_mul_left
deleted theorem dvd_mul_of_dvd_left
deleted theorem dvd_mul_of_dvd_right
deleted theorem dvd_mul_right
deleted def dvd_not_unit
deleted theorem dvd_of_mul_left_dvd
deleted theorem dvd_of_mul_right_dvd
deleted theorem dvd_refl
deleted theorem dvd_rfl
deleted theorem dvd_trans
deleted theorem dvd_zero
deleted theorem eq_zero_of_zero_dvd
deleted theorem exists_eq_mul_left_of_dvd
deleted theorem is_unit.dvd
deleted theorem is_unit.dvd_mul_left
deleted theorem is_unit.dvd_mul_right
deleted theorem is_unit.mul_left_dvd
deleted theorem is_unit.mul_right_dvd
deleted theorem is_unit_iff_dvd_one
deleted theorem is_unit_iff_forall_dvd
deleted theorem is_unit_of_dvd_one
deleted theorem is_unit_of_dvd_unit
deleted theorem map_dvd
deleted theorem monoid_hom.map_dvd
deleted theorem mul_dvd_mul
deleted theorem mul_dvd_mul_iff_left
deleted theorem mul_dvd_mul_iff_right
deleted theorem mul_dvd_mul_left
deleted theorem mul_dvd_mul_right
deleted theorem mul_hom.map_dvd
deleted theorem ne_zero_of_dvd_ne_zero
deleted theorem one_dvd
deleted theorem pow_dvd_pow_of_dvd
deleted theorem units.coe_dvd
deleted theorem units.dvd_mul_left
deleted theorem units.dvd_mul_right
deleted theorem units.mul_left_dvd
deleted theorem units.mul_right_dvd
deleted theorem zero_dvd_iff
added theorem dvd.elim
added theorem dvd.elim_left
added theorem dvd.intro
added theorem dvd.intro_left
added theorem dvd_mul_left
added theorem dvd_mul_of_dvd_left
added theorem dvd_mul_of_dvd_right
added theorem dvd_mul_right
added theorem dvd_of_mul_left_dvd
added theorem dvd_of_mul_right_dvd
added theorem dvd_refl
added theorem dvd_rfl
added theorem dvd_trans
added theorem map_dvd
added theorem monoid_hom.map_dvd
added theorem mul_dvd_mul
added theorem mul_dvd_mul_left
added theorem mul_dvd_mul_right
added theorem mul_hom.map_dvd
added theorem one_dvd
added theorem pow_dvd_pow_of_dvd
added theorem is_unit.dvd
added theorem is_unit.dvd_mul_left
added theorem is_unit.dvd_mul_right
added theorem is_unit.mul_left_dvd
added theorem is_unit.mul_right_dvd
added theorem is_unit_iff_dvd_one
added theorem is_unit_iff_forall_dvd
added theorem is_unit_of_dvd_one
added theorem is_unit_of_dvd_unit
added theorem units.coe_dvd
added theorem units.dvd_mul_left
added theorem units.dvd_mul_right
added theorem units.mul_left_dvd
added theorem units.mul_right_dvd
deleted theorem euclidean_domain.div_zero
deleted theorem euclidean_domain.lt_one
deleted theorem euclidean_domain.mod_lt
deleted theorem euclidean_domain.mod_zero
deleted theorem euclidean_domain.xgcd_val
added theorem dvd_and_not_dvd_iff
added def dvd_not_unit
added theorem dvd_zero
added theorem eq_zero_of_zero_dvd
added theorem mul_dvd_mul_iff_left
added theorem mul_dvd_mul_iff_right
added theorem ne_zero_of_dvd_ne_zero
added theorem zero_dvd_iff
deleted theorem coe_to_units
deleted theorem equiv.coe_mul_left
deleted theorem equiv.coe_mul_right
deleted theorem equiv.mul_left_symm
deleted theorem equiv.mul_left_symm_apply
deleted theorem equiv.mul_right_symm
deleted theorem group.mul_left_bijective
deleted theorem group.mul_right_bijective
deleted def mul_equiv.inv
deleted theorem mul_equiv.inv_symm
deleted theorem mul_left_bijective₀
deleted theorem mul_right_bijective₀
deleted def to_units
deleted theorem units.coe_map_equiv
deleted def units.map_equiv
deleted theorem units.map_equiv_symm
deleted def units.mul_left
deleted theorem units.mul_left_bijective
deleted theorem units.mul_left_symm
deleted def units.mul_right
deleted theorem units.mul_right_bijective
deleted theorem units.mul_right_symm
added theorem coe_to_units
added theorem equiv.coe_mul_left
added theorem equiv.coe_mul_right
added theorem equiv.mul_left_symm
added theorem equiv.mul_right_symm
added def mul_equiv.inv
added theorem mul_equiv.inv_symm
added theorem mul_left_bijective₀
added theorem mul_right_bijective₀
added def to_units
added theorem units.coe_map_equiv
added def units.map_equiv
added theorem units.map_equiv_symm
added def units.mul_left
added theorem units.mul_left_symm
added def units.mul_right
added theorem units.mul_right_symm
deleted theorem eq_on_inv
deleted theorem group.is_unit
deleted theorem is_unit.eq_on_inv
added theorem eq_on_inv
added theorem group.is_unit
added theorem is_unit.eq_on_inv
deleted theorem add_top
deleted theorem bit0_pos
deleted theorem top_add
added theorem add_top
added theorem bit0_pos
added theorem top_add
added structure ring.positive_cone
added structure ring.total_positive_cone
deleted structure ring.positive_cone
deleted structure ring.total_positive_cone
deleted theorem add_le_add_add_tsub
deleted theorem add_tsub_add_eq_tsub_left
deleted theorem add_tsub_add_le_tsub_left
deleted theorem add_tsub_cancel_left
deleted theorem add_tsub_cancel_right
deleted theorem add_tsub_le_assoc
deleted theorem add_tsub_le_left
deleted theorem add_tsub_le_right
deleted theorem add_tsub_le_tsub_add
deleted theorem antitone_const_tsub
deleted theorem eq_tsub_of_add_eq
deleted theorem le_add_tsub'
deleted theorem le_add_tsub
deleted theorem le_add_tsub_swap
deleted theorem le_tsub_add
deleted theorem le_tsub_add_add
deleted theorem le_tsub_of_add_le_left
deleted theorem le_tsub_of_add_le_right
deleted theorem lt_add_of_tsub_lt_left
deleted theorem lt_add_of_tsub_lt_right
deleted theorem lt_of_tsub_lt_tsub_left
deleted theorem lt_of_tsub_lt_tsub_right
deleted theorem lt_tsub_comm
deleted theorem lt_tsub_iff_left
deleted theorem lt_tsub_iff_right
deleted theorem lt_tsub_of_add_lt_left
deleted theorem lt_tsub_of_add_lt_right
deleted theorem tsub_add_eq_tsub_tsub
deleted theorem tsub_eq_of_eq_add
deleted theorem tsub_eq_of_eq_add_rev
deleted theorem tsub_le_iff_left
deleted theorem tsub_le_iff_right
deleted theorem tsub_le_iff_tsub_le
deleted theorem tsub_le_tsub
deleted theorem tsub_le_tsub_add_tsub
deleted theorem tsub_le_tsub_left
deleted theorem tsub_le_tsub_right
deleted theorem tsub_nonpos
deleted theorem tsub_right_comm
deleted theorem tsub_tsub
deleted theorem tsub_tsub_le
deleted theorem tsub_tsub_le_tsub_add
deleted theorem tsub_tsub_tsub_le_tsub
deleted theorem tsub_zero
added theorem add_le_add_add_tsub
added theorem add_tsub_cancel_left
added theorem add_tsub_cancel_right
added theorem add_tsub_le_assoc
added theorem add_tsub_le_left
added theorem add_tsub_le_right
added theorem add_tsub_le_tsub_add
added theorem antitone_const_tsub
added theorem eq_tsub_of_add_eq
added theorem le_add_tsub'
added theorem le_add_tsub
added theorem le_add_tsub_swap
added theorem le_tsub_add
added theorem le_tsub_add_add
added theorem le_tsub_of_add_le_left
added theorem lt_add_of_tsub_lt_left
added theorem lt_tsub_comm
added theorem lt_tsub_iff_left
added theorem lt_tsub_iff_right
added theorem lt_tsub_of_add_lt_left
added theorem tsub_add_eq_tsub_tsub
added theorem tsub_eq_of_eq_add
added theorem tsub_eq_of_eq_add_rev
added theorem tsub_le_iff_left
added theorem tsub_le_iff_right
added theorem tsub_le_iff_tsub_le
added theorem tsub_le_tsub
added theorem tsub_le_tsub_add_tsub
added theorem tsub_le_tsub_left
added theorem tsub_le_tsub_right
added theorem tsub_nonpos
added theorem tsub_right_comm
added theorem tsub_tsub
added theorem tsub_tsub_le
added theorem tsub_tsub_le_tsub_add
added theorem tsub_tsub_tsub_le_tsub
added theorem tsub_zero
deleted theorem mul_one_sub
deleted theorem mul_sub_left_distrib
deleted theorem mul_sub_one
deleted theorem mul_sub_right_distrib
deleted theorem one_sub_mul
deleted theorem sub_one_mul
added theorem mul_one_sub
added theorem mul_sub_left_distrib
added theorem mul_sub_one
added theorem mul_sub_right_distrib
added theorem one_sub_mul
added theorem sub_one_mul