Dedup

📁 Source: Mathlib/Data/Finset/Dedup.lean

Statistics

Metric	Count
Definitions toList, toFinset, toFinset	3
Theorems coe_toList, dedup_eq_self, exists_list_nodup_eq, mem_toList, nodup_toList, perm_toList, toList_toFinset, val_le_iff_val_subset, val_toFinset, coe_toFinset, mem_toFinset, perm_of_nodup_nodup_toFinset_eq, ext, ext_iff, toFinset_coe, toFinset_eq, toFinset_eq_iff_perm_dedup, toFinset_eq_of_perm, toFinset_reverse, toFinset_surj_on, toFinset_surjective, toFinset_toList, toFinset_val, toFinset_inj, isWellFounded_ssubset, mem_toFinset, toFinset_dedup, toFinset_eq, toFinset_ssubset, toFinset_subset, toFinset_val	31
Total	34

Finset

Definitions

Name	Category	Theorems
toList 📖	CompOp	22 math math: toList_insert, toList_cons, Nonempty.not_empty_toList, prod_map_toList, nodup_toList, sum_map_toList, toList_toFinset, List.toFinset_toList, coe_toList, sum_toList, length_toList, toList_empty, prod_toList, Finsupp.toAList_entries, perm_toList, toList_eq_nil, toList_eq_singleton_iff, FirstOrder.Language.Theory.CompleteType.toList_foldr_inf_mem, mem_toList, sort_perm_toList, empty_toList, toList_singleton

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_toList 📖	mathematical	—	Multiset.ofList toList val	—	Multiset.coe_toList
dedup_eq_self 📖	mathematical	—	Multiset.dedup val	—	Multiset.Nodup.dedup nodup
exists_list_nodup_eq 📖	mathematical	—	List.toFinset	—	nodup_toList toList_toFinset
mem_toList 📖	mathematical	—	toList Finset instMembership	—	Multiset.mem_toList
nodup_toList 📖	mathematical	—	toList	—	toList.eq_1 Multiset.coe_nodup Multiset.coe_toList nodup
perm_toList 📖	mathematical	—	toList	—	ext
toList_toFinset 📖	mathematical	—	List.toFinset toList	—	ext
val_le_iff_val_subset 📖	mathematical	—	Multiset Preorder.toLE PartialOrder.toPreorder Multiset.instPartialOrder val Multiset.instHasSubset	—	Multiset.le_iff_subset nodup
val_toFinset 📖	mathematical	—	Multiset.toFinset val	—	ext Multiset.mem_toFinset mem_def

List

Definitions

Name	Category	Theorems
toFinset 📖	CompOp	73 math math: toFinset.ext_iff, mem_toFinset, support_formPerm_le, Finset.sum_filter_count_eq_countP, Fin.univ_image_getElem', sum_toFinset_count_eq_length, foldr_inf_eq_inf_toFinset, toFinset_append, toFinset_range'_1, Finset.prod_list_map_count, Aesop.toFinset_nonempty_of_ne, coe_toFinset, toFinset_filter, toFinset_range'_1_1, toFinset_sort, toFinset_filterMap, RootPairing.EmbeddedG2.indexEquivAllRoots_symm_apply, sum_toFinset, Finset.sum_list_count, toFinset_finRange, SimpleGraph.Walk.IsHamiltonian.support_toFinset, Finset.equivBitIndices_apply, Finset.toList_toFinset, toFinset_eq_iff_perm_dedup, toFinset_toList, toFinset_eq_empty_iff, Nat.toFinset_divisorsAntidiagonalList, Finset.toFinset_bitIndices_twoPowSum, toFinset.ext, card_toFinset, disjoint_toFinset_iff_disjoint, toFinset_surjective, Cycle.coe_toFinset, Fin.univ_image_get', support_formPerm_of_nodup, toFinset_coe, AList.lookupFinsupp_support, Finset.exists_list_nodup_eq, Nat.toFinset_factors, Fin.univ_image_get, zipWith_swap_prod_support', pairwise_iff_coe_toFinset_pairwise, toFinset_card_le, toFinset_reverse, toFinset_range, Fin.univ_image_def, support_formPerm_le', toFinset_surj_on, toFinset_card_of_nodup, Finset.twoPowSum_toFinset_bitIndices, Finset.sort_toFinset, RootPairing.EmbeddedG2.indexEquivAllRoots_apply_coe, toFinset_val, toFinset_inter, Finset.prod_list_count, pairwiseDisjoint_iff_coe_toFinset_pairwise_disjoint, Equiv.Perm.cycleFactorsFinset_eq_list_toFinset, toFinset_cons, toFinset_nonempty_iff, foldr_sup_eq_sup_toFinset, support_formPerm_of_nodup', SimpleGraph.Walk.coe_edges_toFinset, toFinset_eq_of_perm, toFinset_eq, toFinset_replicate_of_ne_zero, Encodable.sortedUniv_toFinset, zipWith_swap_prod_support, toFinset_nil, RootPairing.EmbeddedG2.allRoots_subset_range_root, toFinset_union, Finsupp.toAList_keys_toFinset, Finset.sum_list_map_count, prod_toFinset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_toFinset 📖	mathematical	—	SetLike.coe Finset Finset.instSetLike toFinset setOf	—	Set.ext mem_toFinset
mem_toFinset 📖	mathematical	—	Finset Finset.instMembership toFinset	—	mem_dedup
perm_of_nodup_nodup_toFinset_eq 📖	—	toFinset	—	—	Multiset.coe_eq_coe
toFinset_coe 📖	mathematical	—	Multiset.toFinset Multiset.ofList toFinset	—	—
toFinset_eq 📖	mathematical	—	Multiset.ofList toFinset	—	Multiset.toFinset_eq Multiset.coe_nodup
toFinset_eq_iff_perm_dedup 📖	mathematical	—	toFinset dedup	—	nodup_dedup
toFinset_eq_of_perm 📖	mathematical	—	toFinset	—	toFinset_eq_iff_perm_dedup Perm.dedup
toFinset_reverse 📖	mathematical	—	toFinset	—	toFinset_eq_of_perm
toFinset_surj_on 📖	mathematical	—	Set.SurjOn Finset toFinset setOf Set.univ	—	toFinset_eq
toFinset_surjective 📖	mathematical	—	Finset toFinset	—	toFinset_surj_on Set.mem_univ
toFinset_toList 📖	mathematical	—	Finset.toList toFinset	—	perm_of_nodup_nodup_toFinset_eq Finset.nodup_toList Finset.toList_toFinset
toFinset_val 📖	mathematical	—	Finset.val toFinset Multiset.ofList dedup	—	—

List.toFinset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	mathematical	—	List.toFinset	—	ext_iff
ext_iff 📖	mathematical	—	List.toFinset	—	—

Multiset

Definitions

Name	Category	Theorems
toFinset 📖	CompOp	112 math math: Ideal.pow_multiset_sum_mem_span_pow, Finset.prod_multiset_map_count, Submodule.isInternal_prime_power_torsion_of_pid, toDFinsupp_support, Equiv.Perm.card_of_cycleType_mul_eq, Finset.val_toFinset, card_Ico, Ideal.Factors.fact_ramificationIdx_neZero, toFinset_cons, toFinset_filter, toFinset_sum_count_eq, toFinset_eq_empty, IsPrimitiveRoot.is_roots_of_minpoly, Finset.sym2_toFinset, Polynomial.rootsExpandPowEquivRoots_apply, Equiv.Perm.OnCycleFactors.nat_card_range_toPermHom, Finset.image_toFinset, toFinset_card_le, Submodule.isInternal_prime_power_torsion_of_is_torsion_by_ideal, UniqueFactorizationMonoid.factors_pow_count_prod, Finset.map_comp_coe_apply, Polynomial.prod_multiset_root_eq_finset_root, Polynomial.rootsExpandEquivRoots_apply, Polynomial.card_roots_toFinset_le_card_roots_derivative_diff_roots_succ, toFinset_nsmul, PMF.mem_support_ofMultiset_iff, toFinset_add, Cubic.card_roots_of_disc_ne_zero, Cubic.card_roots_of_discr_ne_zero, card_Ioc, Polynomial.roots_expand_image_frobenius, bell_mul_eq, Polynomial.bUnion_roots_finite, Ideal.Factors.isScalarTower, Polynomial.rootsExpandPowToRoots_apply, Equiv.Perm.card_isConj_eq, toFinset_prod_dvd_prod, card_uIcc, card_le_card_toFinset_add_one_iff, Equiv.Perm.card_of_cycleType, DFinsupp.support_mk'_subset, Polynomial.eq_centerMass_of_eval_derivative_eq_zero, Polynomial.roots_expand_image_frobenius_subset, Polynomial.rootSet_def, Finset.map_toFinset, PMF.support_ofMultiset, List.toFinset_coe, AlternatingGroup.card_of_cycleType, Nat.sum_divisors_filter_squarefree, toFinset_range, Finset.map_comp_coe, Ideal.Factors.liesOver, toFinset_zero, MvPolynomial.vars_def, toFinset_replicate, disjoint_toFinset, card_toFinset, Polynomial.sum_derivRootWeight_pos, Finset.sum_multiset_map_count, toFinset_card_eq_one_iff, toFinset_union, bell_eq, Ideal.Factors.finrank_pow_ramificationIdx, Polynomial.rootsExpandToRoots_apply, Finsupp.toFinset_toMultiset, Aesop.toFinset_nonempty_of_ne, Cycle.toFinset_toMultiset, toFinset_card_of_nodup, finite_toSet_toFinset, toFinset_card_eq_card_iff_nodup, Submodule.isInternal_prime_power_torsion, Polynomial.natSepDegree_eq_of_isAlgClosed, toFinset_subset, Finset.sum_mem_multiset, card_Iic, Cubic.card_roots_le, Polynomial.roots_expand_image_iterateFrobenius, Polynomial.nthRootsFinset_def, toFinset_inter, Polynomial.roots_expand_pow_image_iterateFrobenius_subset, toFinset_dedup, toFinset_eq, toFinset_ssubset, Ideal.Factors.finiteDimensional_quotient_pow, Finset.prod_mem_multiset, card_Icc, toFinset_map, Ideal.Factors.isPrime, Finset.sup_toFinset, Nat.divisors_filter_squarefree, toFinset_sum_count_nsmul_eq, Polynomial.natSepDegree_eq_of_splits, Finset.prod_multiset_count, image_toEnumFinset_fst, Finset.sum_multiset_count, Ideal.Factors.piQuotientEquiv_mk, card_Ioo, toFinsupp_support, mem_toFinset, Polynomial.card_roots_toFinset_le_derivative, IsDedekindDomain.quotientEquivPiFactors_mk, toFinset_singleton, AlternatingGroup.card_of_cycleType_mul_eq, support_factorization, Polynomial.normalizedFactors_cyclotomic_card, Equiv.Perm.card_isConj_mul_eq, Equiv.Perm.nat_card_centralizer, Ideal.Factors.piQuotientEquiv_map, Finset.bind_toFinset, toFinset_nonempty, toFinset_eq_singleton_iff, toFinset_val

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isWellFounded_ssubset 📖	mathematical	—	IsWellFounded Multiset instHasSSubset	—	Subrelation.isWellFounded instIsWellFoundedInvImage Finset.isWellFounded_ssubset toFinset_ssubset
mem_toFinset 📖	mathematical	—	Finset Finset.instMembership toFinset Multiset instMembership	—	mem_dedup
toFinset_dedup 📖	mathematical	—	toFinset dedup	—	nodup_dedup dedup_idem
toFinset_eq 📖	mathematical	Nodup	toFinset	—	Nodup.dedup
toFinset_ssubset 📖	mathematical	—	Finset Finset.instHasSSubset toFinset Multiset instHasSSubset	—	—
toFinset_subset 📖	mathematical	—	Finset Finset.instHasSubset toFinset Multiset instHasSubset	—	—
toFinset_val 📖	mathematical	—	Finset.val toFinset dedup	—	—

Multiset.Nodup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toFinset_inj 📖	—	Multiset.Nodup Multiset.toFinset	—	—	Multiset.toFinset_eq

---

← Back to Index