Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-01-16 07:12 47adfab3

View on Github →

chore(*): sync list.replicate with Mathlib 4 (#18181) Sync arguments order and golfs with leanprover-community/mathlib4#1579

Estimated changes

modified theorem multiset.prod_replicate
modified theorem list.append_left_injective
modified theorem list.append_right_injective
modified theorem list.eq_of_mem_map_const
modified theorem list.last_replicate_succ
added theorem list.map_const'
modified theorem list.map_const
modified theorem list.map_replicate
modified theorem list.replicate_add
added theorem list.replicate_one
added theorem list.replicate_succ'
added theorem list.replicate_zero
modified theorem list.reverse_replicate
modified theorem list.prod_replicate
modified theorem list.sum_const_nat
added theorem list.filter_eq'
added theorem list.filter_eq
modified theorem list.perm_replicate
modified theorem list.replicate_perm
modified theorem multiset.coe_replicate
added theorem multiset.map_const'
modified theorem multiset.replicate_add
modified theorem multiset.replicate_inter
modified theorem multiset.replicate_one
modified theorem multiset.replicate_succ