Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-31 07:34 b7f120f1

View on Github →

chore(*): clean up the library using to_additive (#9790) Since #9138 and #5487 to_additive got a lot better, so a lot of duplication in the library becomes unnecessary and makes maintenence a burden. So we remove a large number of copy-pasted declarations that can now be generated automatically.

Estimated changes

modified theorem finset.pow_eq_prod_const
modified theorem finset.prod_const
deleted theorem finset.sum_const
deleted theorem finset.sum_nsmul
deleted theorem finset.sum_update_of_mem
deleted theorem nsmul_one'
deleted theorem add_monoid_hom.map_zsmul
deleted theorem add_one_zsmul
deleted theorem add_zsmul
deleted theorem bit0_zsmul
deleted theorem bit1_zsmul
modified theorem commute.units_zpow_left
modified theorem commute.units_zpow_right
modified theorem monoid_hom.map_zpow
deleted theorem mul_zsmul
deleted theorem one_add_zsmul
deleted theorem sub_zsmul
modified theorem units.coe_pow
modified theorem units.coe_zpow
deleted theorem zsmul_add_comm
deleted theorem zsmul_mul'
deleted theorem add_left_iterate
deleted theorem add_right_iterate
modified theorem mul_left_iterate
modified theorem mul_right_iterate
deleted theorem list.sum_take_of_fn
deleted theorem is_add_submonoid.smul_mem
deleted theorem multiples.add_mem
deleted theorem multiples.self_mem
deleted theorem multiples.zero_mem
deleted def multiples
deleted theorem add_order_of_eq_one_iff
deleted theorem add_order_of_eq_prime_pow
deleted theorem add_order_of_injective
deleted theorem add_order_of_le_card_univ
deleted theorem add_order_of_nsmul''
deleted theorem add_order_of_nsmul'
deleted theorem add_order_of_nsmul
deleted theorem add_order_of_pos
deleted theorem add_order_of_zero
deleted theorem card_nsmul_eq_zero
deleted theorem exists_nsmul_eq_zero
deleted theorem exists_zsmul_eq_zero
deleted theorem fin_equiv_multiples_apply
modified theorem fin_equiv_powers_apply
modified theorem fin_equiv_powers_symm_apply
modified theorem fin_equiv_zpowers_apply
deleted theorem multiples_eq_zmultiples
deleted theorem nsmul_eq_mod_add_order_of
deleted theorem nsmul_inj_mod
deleted theorem nsmul_injective_aux
modified theorem order_of_eq_one_iff
modified theorem order_of_one
modified theorem pow_card_eq_one
deleted theorem zsmul_eq_mod_add_order_of
deleted theorem add_subgroup.coe_smul
deleted theorem add_subgroup.coe_zsmul
modified theorem subgroup.coe_copy
modified theorem subgroup.coe_pow
modified theorem subgroup.coe_zpow