Commit 2023-01-16 07:17 75764ca4

View on Github →

Refactor: drop List.repeat (#1579) Mathlib 3 migrated to list.replicate in leanprover-community/mathlib#18127 (merged) and leanprover-community/mathlib#18181 (awaiting review).

Estimated changes

modified theorem Multiset.prod_map_one
deleted theorem Multiset.prod_repeat
modified theorem List.eq_of_mem_map_const
deleted theorem List.eq_of_mem_repeat
deleted theorem List.eq_repeat'
deleted theorem List.eq_repeat
deleted theorem List.eq_repeat_of_mem
deleted theorem List.eq_replicate'
modified theorem List.eq_replicate
deleted theorem List.eq_replicate_of_mem
deleted theorem List.getLast_repeat_succ
modified theorem List.getLast_replicate_succ
deleted theorem List.join_repeat_nil
modified theorem List.join_replicate_nil
deleted theorem List.length_repeat
modified theorem List.map_const'
modified theorem List.map_const
deleted theorem List.map_eq_repeat_iff
deleted theorem List.map_repeat
modified theorem List.map_replicate
deleted theorem List.mem_repeat
deleted theorem List.nthLe_repeat
added theorem List.nthLe_replicate
deleted theorem List.repeat_add
deleted theorem List.repeat_left_inj'
deleted theorem List.repeat_left_inj
deleted theorem List.repeat_right_inj
deleted theorem List.repeat_succ
modified theorem List.replicate_add
deleted theorem List.replicate_left_inj'
modified theorem List.replicate_left_inj
added theorem List.replicate_one
modified theorem List.replicate_right_inj
added theorem List.replicate_succ'
added theorem List.replicate_zero
deleted theorem List.reverse_repeat
modified theorem List.reverse_replicate
deleted theorem List.sublist_repeat_iff
modified theorem List.subset_singleton_iff
deleted theorem List.tail_repeat
deleted theorem List.take_repeat
modified theorem List.take_replicate
modified theorem List.headI_add_tail_sum
deleted theorem List.prod_repeat
modified theorem List.prod_replicate
modified theorem List.sum_const_nat
deleted theorem List.count_repeat
deleted theorem List.count_repeat_self
added theorem List.filter_beq'
added theorem List.filter_beq
added theorem List.filter_eq'
added theorem List.filter_eq
deleted theorem List.repeat_dedup
deleted theorem List.nodup_repeat
deleted theorem List.pairwise_repeat
deleted theorem List.perm_repeat
modified theorem List.perm_replicate
deleted theorem List.repeat_perm
modified theorem List.replicate_perm
deleted theorem Multiset.card_repeat
deleted theorem Multiset.coe_repeat
added theorem Multiset.coe_replicate
modified theorem Multiset.count_cons_self
modified theorem Multiset.count_erase_self
deleted theorem Multiset.count_repeat
deleted theorem Multiset.eq_of_mem_repeat
deleted theorem Multiset.eq_repeat'
deleted theorem Multiset.eq_repeat
deleted theorem Multiset.eq_repeat_of_mem
added theorem Multiset.eq_replicate
modified theorem Multiset.filter_eq'
modified theorem Multiset.filter_eq
deleted theorem Multiset.inter_repeat
deleted theorem Multiset.le_repeat_iff
deleted theorem Multiset.lt_repeat_succ
modified theorem Multiset.map_const'
modified theorem Multiset.map_const
deleted theorem Multiset.map_repeat
added theorem Multiset.map_replicate
deleted theorem Multiset.mem_repeat
added theorem Multiset.mem_replicate
deleted theorem Multiset.nsmul_repeat
modified theorem Multiset.nsmul_singleton
deleted theorem Multiset.rel_repeat_left
deleted theorem Multiset.rel_repeat_right
deleted theorem Multiset.repeat_add
deleted theorem Multiset.repeat_inf
deleted theorem Multiset.repeat_injective
deleted theorem Multiset.repeat_inter
deleted theorem Multiset.repeat_le_coe
deleted theorem Multiset.repeat_le_repeat
deleted theorem Multiset.repeat_left_inj
deleted theorem Multiset.repeat_one
deleted theorem Multiset.repeat_succ
deleted theorem Multiset.repeat_zero
added theorem Multiset.replicate_add
added theorem Multiset.replicate_one
deleted def Multiset.«repeat»
added def Vector.replicate
deleted def Vector.«repeat»
deleted def List.«repeat»