Commit 2023-01-15 06:15 f694c7de

View on Github →

refactor(*): define list.replicate and migrate to it (#18127) This definition differs from list.repeat by the order of arguments. The new order is in sync with the Lean 4 version.

Estimated changes

Modified archive/100-theorems-list/30_ballot_problem.lean

modified theorem ballot.counted_left_zero

modified theorem ballot.counted_right_zero

Modified archive/100-theorems-list/45_partition.lean

Modified archive/miu_language/decision_suf.lean

deleted theorem miu.der_cons_repeat_I_repeat_U_append_of_der_cons_repeat_I_append

added theorem miu.der_cons_replicate_I_replicate_U_append_of_der_cons_replicate_I_append

deleted theorem miu.der_of_der_append_repeat_U_even

added theorem miu.der_of_der_append_replicate_U_even

deleted theorem miu.der_repeat_I_of_mod3

added theorem miu.der_replicate_I_of_mod3

deleted theorem miu.repeat_pow_minus_append

added theorem miu.replicate_pow_minus_append

Modified src/algebra/big_operators/basic.lean

Modified src/algebra/big_operators/multiset/basic.lean

modified theorem multiset.prod_map_one

deleted theorem multiset.prod_repeat

added theorem multiset.prod_replicate

Modified src/algebra/gcd_monoid/multiset.lean

Modified src/algebra/hom/freiman.lean

Modified src/algebra/module/dedekind_domain.lean

Modified src/algebra/monoid_algebra/degree.lean

Modified src/algebra/polynomial/big_operators.lean

Modified src/combinatorics/composition.lean

modified theorem composition.ones_blocks

Modified src/computability/turing_machine.lean

Modified src/data/bitvec/core.lean

Modified src/data/dfinsupp/multiset.lean

deleted theorem multiset.to_dfinsupp_repeat

added theorem multiset.to_dfinsupp_replicate

Modified src/data/finset/basic.lean

deleted theorem list.to_finset_repeat_of_ne_zero

added theorem list.to_finset_replicate_of_ne_zero

Modified src/data/finset/sym.lean

deleted theorem finset.repeat_mem_sym

added theorem finset.replicate_mem_sym

modified theorem finset.sym_singleton

Modified src/data/fintype/card.lean

Modified src/data/list/basic.lean

deleted theorem list.eq_of_mem_repeat

added theorem list.eq_of_mem_replicate

deleted theorem list.eq_repeat'

deleted theorem list.eq_repeat

deleted theorem list.eq_repeat_of_mem

added theorem list.eq_replicate

added theorem list.eq_replicate_length

deleted theorem list.join_repeat_nil

added theorem list.join_replicate_nil

deleted theorem list.last_repeat_succ

added theorem list.last_replicate_succ

added theorem list.length_replicate

modified theorem list.map_const

deleted theorem list.map_eq_repeat_iff

added theorem list.map_eq_replicate_iff

deleted theorem list.map_repeat

added theorem list.map_replicate

deleted theorem list.mem_repeat

added theorem list.mem_replicate

deleted theorem list.nth_le_repeat

added theorem list.nth_le_replicate

deleted theorem list.nthd_repeat_default_eq

added theorem list.nthd_replicate_default_eq

deleted theorem list.repeat_add

deleted theorem list.repeat_left_inj'

deleted theorem list.repeat_left_inj

deleted theorem list.repeat_left_injective

deleted theorem list.repeat_right_inj

deleted theorem list.repeat_right_injective

deleted theorem list.repeat_sublist_repeat

deleted theorem list.repeat_subset_singleton

deleted theorem list.repeat_succ

added theorem list.replicate_add

added theorem list.replicate_left_inj

added theorem list.replicate_left_injective

added theorem list.replicate_right_inj'

added theorem list.replicate_right_inj

added theorem list.replicate_right_injective

added theorem list.replicate_sublist_replicate

added theorem list.replicate_subset_singleton

added theorem list.replicate_succ

deleted theorem list.reverse_repeat

added theorem list.reverse_replicate

deleted theorem list.sublist_repeat_iff

added theorem list.sublist_replicate_iff

modified theorem list.subset_singleton_iff

deleted theorem list.tail_repeat

added theorem list.tail_replicate

modified theorem list.take'_nil

deleted theorem list.take_repeat

added theorem list.take_replicate

Modified src/data/list/big_operators/basic.lean

deleted theorem list.prod_repeat

added theorem list.prod_replicate

modified theorem list.sum_const_nat

Modified src/data/list/big_operators/lemmas.lean

Modified src/data/list/count.lean

deleted theorem list.count_repeat

deleted theorem list.count_repeat_self

added theorem list.count_replicate

added theorem list.count_replicate_self

deleted theorem list.le_count_iff_repeat_sublist

added theorem list.le_count_iff_replicate_sublist

deleted theorem list.repeat_count_eq_of_count_eq_length

added theorem list.replicate_count_eq_of_count_eq_length

Modified src/data/list/dedup.lean

deleted theorem list.repeat_dedup

added theorem list.replicate_dedup

Modified src/data/list/defs.lean

added def list.replicate

Modified src/data/list/duplicate.lean

Modified src/data/list/nodup.lean

deleted theorem list.nodup_repeat

added theorem list.nodup_replicate

Modified src/data/list/nodup_equiv_fin.lean

Modified src/data/list/of_fn.lean

Modified src/data/list/pairwise.lean

deleted theorem list.pairwise_repeat

added theorem list.pairwise_replicate

Modified src/data/list/perm.lean

deleted theorem list.perm.eq_singleton

deleted theorem list.perm.singleton_eq

deleted theorem list.perm_repeat

deleted theorem list.perm_repeat_append_repeat

added theorem list.perm_replicate

added theorem list.perm_replicate_append_replicate

deleted theorem list.repeat_perm

added theorem list.replicate_perm

Modified src/data/list/rotate.lean

deleted theorem list.rotate_eq_self_iff_eq_repeat

added theorem list.rotate_eq_self_iff_eq_replicate

modified theorem list.rotate_injective

deleted theorem list.rotate_one_eq_self_iff_eq_repeat

added theorem list.rotate_one_eq_self_iff_eq_replicate

deleted theorem list.rotate_repeat

added theorem list.rotate_replicate

Modified src/data/list/sigma.lean

Modified src/data/list/sort.lean

Modified src/data/multiset/basic.lean

deleted theorem multiset.card_repeat

added theorem multiset.card_replicate

deleted theorem multiset.coe_repeat

added theorem multiset.coe_replicate

deleted theorem multiset.count_repeat

deleted theorem multiset.count_repeat_self

added theorem multiset.count_replicate

added theorem multiset.count_replicate_self

deleted theorem multiset.eq_of_mem_repeat

added theorem multiset.eq_of_mem_replicate

deleted theorem multiset.eq_repeat'

deleted theorem multiset.eq_repeat

deleted theorem multiset.eq_repeat_of_mem

added theorem multiset.eq_replicate

added theorem multiset.eq_replicate_card

modified theorem multiset.filter_eq'

modified theorem multiset.filter_eq

deleted theorem multiset.inter_repeat

added theorem multiset.inter_replicate

deleted theorem multiset.le_count_iff_repeat_le

added theorem multiset.le_count_iff_replicate_le

deleted theorem multiset.le_repeat_iff

added theorem multiset.le_replicate_iff

deleted theorem multiset.lt_repeat_succ

added theorem multiset.lt_replicate_succ

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

added theorem multiset.nsmul_replicate

modified theorem multiset.nsmul_singleton

deleted theorem multiset.rel_repeat_left

deleted theorem multiset.rel_repeat_right

added theorem multiset.rel_replicate_left

added theorem multiset.rel_replicate_right

deleted def multiset.repeat

deleted theorem multiset.repeat_add

deleted def multiset.repeat_add_monoid_hom

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_left_injective

deleted theorem multiset.repeat_one

deleted theorem multiset.repeat_subset_singleton

deleted theorem multiset.repeat_succ

deleted theorem multiset.repeat_zero

added def multiset.replicate

added theorem multiset.replicate_add

added def multiset.replicate_add_monoid_hom

added theorem multiset.replicate_inter

added theorem multiset.replicate_le_coe

added theorem multiset.replicate_le_replicate

added theorem multiset.replicate_left_injective

added theorem multiset.replicate_one

added theorem multiset.replicate_right_inj

added theorem multiset.replicate_right_injective

added theorem multiset.replicate_subset_singleton

added theorem multiset.replicate_succ

added theorem multiset.replicate_zero

Modified src/data/multiset/bind.lean

modified theorem multiset.card_product

Modified src/data/multiset/interval.lean

Modified src/data/multiset/nodup.lean

Modified src/data/nat/choose/multinomial.lean

Modified src/data/nat/digits.lean

modified def nat.digits_aux_1

modified theorem nat.digits_one

Modified src/data/nat/factorization/basic.lean

Modified src/data/nat/factors.lean

Modified src/data/pnat/factors.lean

Modified src/data/polynomial/ring_division.lean

Modified src/data/polynomial/splits.lean

Modified src/data/qpf/multivariate/constructions/cofix.lean

Modified src/data/set/pointwise/list_of_fn.lean

Modified src/data/sym/basic.lean

deleted theorem sym.coe_repeat

added theorem sym.coe_replicate

deleted theorem sym.eq_repeat

deleted theorem sym.eq_repeat_iff

deleted theorem sym.eq_repeat_of_subsingleton

added theorem sym.eq_replicate

added theorem sym.eq_replicate_iff

added theorem sym.eq_replicate_of_subsingleton

deleted theorem sym.mem_repeat

added theorem sym.mem_replicate

deleted def sym.repeat

deleted theorem sym.repeat_left_inj

deleted theorem sym.repeat_left_injective

deleted theorem sym.repeat_succ

added def sym.replicate

added theorem sym.replicate_right_inj

added theorem sym.replicate_right_injective

added theorem sym.replicate_succ

Modified src/data/vector/basic.lean

deleted theorem vector.nth_repeat

added theorem vector.nth_replicate

added def vector.replicate

Modified src/field_theory/abel_ruffini.lean

Modified src/group_theory/p_group.lean

Modified src/group_theory/perm/cycle/type.lean

Modified src/group_theory/perm/sign.lean

Modified src/group_theory/specific_groups/alternating.lean

Modified src/logic/equiv/list.lean

Modified src/number_theory/arithmetic_function.lean

Modified src/number_theory/ramification_inertia.lean

Modified src/ring_theory/chain_of_divisors.lean

Modified src/ring_theory/dedekind_domain/ideal.lean

Modified src/ring_theory/discrete_valuation_ring.lean

Modified src/ring_theory/polynomial/vieta.lean

Modified src/ring_theory/unique_factorization_domain.lean

deleted theorem unique_factorization_monoid.le_multiplicity_iff_repeat_le_normalized_factors

added theorem unique_factorization_monoid.le_multiplicity_iff_replicate_le_normalized_factors

Modified src/set_theory/ordinal/fixed_point.lean

Modified src/tactic/explode.lean

Modified src/tactic/induction.lean

Modified src/tactic/omega/prove_unsats.lean

deleted theorem omega.forall_mem_repeat_zero_eq_zero

added theorem omega.forall_mem_replicate_zero_eq_zero

Modified src/tactic/solve_by_elim.lean

Modified src/tactic/unify_equations.lean