Replicate

📁 Source: Mathlib/Data/Multiset/Replicate.lean

Statistics

Metric	Count
Definitions replicate	1
Theorems pairwise, card_replicate, coe_replicate, count_replicate, count_replicate_self, eq_of_mem_replicate, eq_replicate, eq_replicate_card, eq_replicate_of_mem, le_count_iff_replicate_le, le_replicate_iff, lt_replicate_succ, mem_replicate, nodup_iff_le, nodup_iff_ne_cons_cons, nodup_iff_pairwise, rel_replicate_left, rel_replicate_right, replicate_add, replicate_le_coe, replicate_le_replicate, replicate_left_injective, replicate_mono, replicate_one, replicate_right_inj, replicate_right_injective, replicate_subset_singleton, replicate_succ, replicate_zero	29
Total	30

Multiset

Definitions

Name	Category	Theorems
replicate 📖	CompOp	49 math math: prod_replicate, replicate_right_inj, count_replicate, replicate_left_injective, card_replicate, eq_replicate_of_mem, DFinsupp.toMultiset_single, Polynomial.nthRoots_zero_right, replicate_succ, map_const, Equiv.Perm.cycleType_prime_order, replicate_le_replicate, toDFinsupp_replicate, replicate_inter, Associates.factors_prime_pow, map_replicate, filter_eq, replicate_add, rel_replicate_left, replicateAddMonoidHom_apply, mem_replicate, sum_replicate, toFinset_replicate, nsmul_replicate, Irreducible.normalizedFactors_pow, eq_replicate, replicate_subset_singleton, Equiv.Perm.cycleType_of_pow_prime_eq_one, UniqueFactorizationMonoid.le_emultiplicity_iff_replicate_le_normalizedFactors, filter_eq', nsmul_singleton, le_count_iff_replicate_le, le_replicate_iff, replicate_zero, Equiv.Perm.parts_partition, UniqueFactorizationMonoid.normalizedFactors_of_irreducible_pow, rel_replicate_right, Sym.coe_replicate, eq_replicate_card, count_replicate_self, coe_replicate, replicate_right_injective, replicate_mono, replicate_le_coe, map_const', replicate_one, lt_replicate_succ, Sym.val_replicate, inter_replicate

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_replicate 📖	mathematical	—	card replicate	—	—
coe_replicate 📖	mathematical	—	ofList replicate	—	—
count_replicate 📖	mathematical	—	count replicate	—	coe_count coe_replicate
count_replicate_self 📖	mathematical	—	count replicate	—	coe_count coe_replicate
eq_of_mem_replicate 📖	—	Multiset instMembership replicate	—	—	—
eq_replicate 📖	mathematical	—	replicate card	—	card_replicate eq_of_mem_replicate eq_replicate_of_mem
eq_replicate_card 📖	mathematical	—	replicate card	—	coe_eq_coe List.eq_replicate_length
eq_replicate_of_mem 📖	mathematical	—	replicate card	—	eq_replicate_card
le_count_iff_replicate_le 📖	mathematical	—	count Multiset Preorder.toLE PartialOrder.toPreorder instPartialOrder replicate	—	coe_count replicate_le_coe
le_replicate_iff 📖	mathematical	—	Multiset Preorder.toLE PartialOrder.toPreorder instPartialOrder replicate	—	LE.le.trans_eq card_mono card_replicate eq_replicate_card eq_of_mem_replicate subset_of_le replicate_le_replicate
lt_replicate_succ 📖	mathematical	—	Multiset Preorder.toLT PartialOrder.toPreorder instPartialOrder replicate Preorder.toLE	—	lt_iff_cons_le eq_of_mem_replicate mem_of_le mem_cons_self cons_le_cons_iff replicate_succ cons_le_cons
mem_replicate 📖	mathematical	—	Multiset instMembership replicate	—	—
nodup_iff_le 📖	mathematical	—	Nodup Multiset Preorder.toLE PartialOrder.toPreorder instPartialOrder cons instZero	—	Quot.induction_on List.nodup_iff_sublist replicate_le_coe
nodup_iff_ne_cons_cons 📖	mathematical	—	Nodup	—	nodup_iff_le cons_le_cons zero_le le_iff_exists_add zero_add cons_add
nodup_iff_pairwise 📖	mathematical	—	Nodup Pairwise	—	pairwise_coe_iff_pairwise
rel_replicate_left 📖	mathematical	—	Rel replicate card	—	card_eq_card_of_rel card_replicate exists_mem_of_rel_of_mem rel_flip eq_of_mem_replicate rel_of_forall
rel_replicate_right 📖	mathematical	—	Rel replicate card	—	rel_flip rel_replicate_left
replicate_add 📖	mathematical	—	replicate Multiset instAdd	—	List.replicate_add
replicate_le_coe 📖	mathematical	—	Multiset Preorder.toLE PartialOrder.toPreorder instPartialOrder replicate ofList	—	—
replicate_le_replicate 📖	mathematical	—	Multiset Preorder.toLE PartialOrder.toPreorder instPartialOrder replicate	—	trans IsPreorder.toIsTrans IsEquiv.toIsPreorder iff_isEquiv replicate_le_coe coe_replicate
replicate_left_injective 📖	mathematical	—	Multiset replicate	—	card_replicate
replicate_mono 📖	mathematical	—	Multiset Preorder.toLE PartialOrder.toPreorder instPartialOrder replicate	—	replicate_le_replicate
replicate_one 📖	mathematical	—	replicate Multiset instSingleton	—	—
replicate_right_inj 📖	mathematical	—	replicate	—	replicate_right_injective
replicate_right_injective 📖	mathematical	—	Multiset replicate	—	eq_replicate mem_replicate
replicate_subset_singleton 📖	mathematical	—	Multiset instHasSubset replicate instSingleton	—	List.replicate_subset_singleton
replicate_succ 📖	mathematical	—	replicate cons	—	—
replicate_zero 📖	mathematical	—	replicate Multiset instZero	—	—

Multiset.Nodup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
pairwise 📖	mathematical	Multiset.Nodup	Multiset.Pairwise	—	—

---

← Back to Index