Sym

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

Statistics

Metric	Count
Definitions sym2, Sym	2
Theorems sym2, card_sym2, dedup_sym2, mem_sym2_iff, mk_mem_sym2_iff, monotone_sym2, setOf_mem_sym2, sym2_coe, sym2_cons, sym2_eq_zero_iff, sym2_map, sym2_mono, sym2_zero	13
Total	15

Multiset

Definitions

Name	Category	Theorems
sym2 📖	CompOp	15 math math: Nodup.sym2, Finset.sym2_toFinset, setOf_mem_sym2, mk_mem_sym2_iff, sym2_eq_zero_iff, mem_sym2_iff, sym2_zero, sym2_mono, sym2_cons, dedup_sym2, Finset.sym2_val, sym2_map, monotone_sym2, sym2_coe, card_sym2

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_sym2 📖	mathematical	—	card Sym2 sym2 Nat.choose	—	List.length_sym2
dedup_sym2 📖	mathematical	—	dedup Sym2 Sym2.instDecidableEq sym2	—	List.dedup_sym2
mem_sym2_iff 📖	mathematical	—	Sym2 Multiset instMembership sym2	—	—
mk_mem_sym2_iff 📖	mathematical	—	Sym2 Multiset instMembership sym2	—	—
monotone_sym2 📖	mathematical	—	Monotone Multiset Sym2 PartialOrder.toPreorder instPartialOrder sym2	—	sym2_mono
setOf_mem_sym2 📖	mathematical	—	setOf Sym2 Multiset instMembership sym2 Set.sym2	—	Set.ext Sym2.ind
sym2_coe 📖	mathematical	—	sym2 ofList Sym2 List.sym2	—	—
sym2_cons 📖	mathematical	—	sym2 cons Multiset Sym2 instAdd map	—	—
sym2_eq_zero_iff 📖	mathematical	—	sym2 Multiset Sym2 instZero	—	—
sym2_map 📖	mathematical	—	sym2 map Sym2 Sym2.map	—	List.sym2_map
sym2_mono 📖	mathematical	Multiset Preorder.toLE PartialOrder.toPreorder instPartialOrder	Multiset Sym2 Preorder.toLE PartialOrder.toPreorder instPartialOrder sym2	—	List.Subperm.sym2
sym2_zero 📖	mathematical	—	sym2 Multiset instZero Sym2	—	—

Multiset.Nodup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
sym2 📖	mathematical	Multiset.Nodup	Multiset.Nodup Sym2 Multiset.sym2	—	List.Nodup.sym2

(root)

Definitions

Name	Category	Theorems
Sym 📖	CompOp	89 math math: Sym.toMultiset_zero, SymOptionSuccEquiv.encode_of_none_notMem, Finset.sym_univ, Sym.fill_filterNe, Finset.mem_sym_iff, Sym.coe_equivNatSumOfFintype_apply_apply, Sym.mem_map, Sym.coe_equivNatSum_apply_apply, SymOptionSuccEquiv.decode_inr, Finset.sym_nonempty, Sym.coe_equivNatSum_symm_apply, Sym.cast_rfl, List.Sublist.sym, Finset.map_sym_eq_piAntidiag, Sym.exists, Finset.count_coe_finsuppAntidiagEquiv_apply, DividedPowers.dpow_sum', Sym.coe_equivNatSumOfFintype_symm_apply, Sym.mem_fill_iff, Finset.Nonempty.sym, Sym.mem_mk, Sym.card_sym_eq_choose, Finset.replicate_mem_sym, Sym.instSubsingleton, Finset.sym_union, Sym.equivCongr_apply, Sym.mem_replicate, Sym.instIsEmptySucc, norm_iteratedFDerivWithin_prod_le, Sym.attach_nil, Sym.attach_map_coe, DividedPowers.dpow_sum, Sym.cast_cast, Sym.instNontrivialHAddNatOfNat, Finset.sum_pow_of_commute, Sym.map_injective, Finset.sym_inter, Finset.sym_zero, List.sym_map, Sym.map_zero, Sym.filter_ne_fill, Sym.mem_cast, Sym.mem_cons_self, instFiniteSym, Sym.cons_equiv_eq_equiv_cons, List.length_sym, Finset.sym_map, Finset.sym_fill_mem, Finset.sym_singleton, Sym.append_comm, Finset.sym_eq_empty, SymOptionSuccEquiv.encode_of_none_mem, Sym.equivCongr_symm_apply, Finset.sym_filterNe_mem, DividedPowerAlgebra.dp_sum_smul, DividedPowers.dpow_linearCombination, norm_iteratedFDeriv_prod_le, SymOptionSuccEquiv.decode_inl, Sym.card_sym_fin_eq_multichoose, DividedPowerAlgebra.dp_sum, Sym.coe_injective, Sym.replicate_right_injective, Sym.mem_append_iff, Sym.notMem_nil, Sym.exists_mem, List.sym_sublist_sym_cons, Sym.attach_cons, Sym.mem_cons_of_mem, List.sym_one_eq, Finset.symInsertEquiv_apply_snd_coe, List.Nodup.sym, Sym.oneEquiv_apply, Finset.symInsertEquiv_apply_fst, Finset.sym_empty, Sym.coe_cast, Sym.mem_coe, Finset.symInsertEquiv_symm_apply_coe, Sym.mem_attach, Finset.sym_succ, Finset.sum_pow, Sym.mem_cons, Sym.card_sym_eq_multichoose, Finset.finsuppAntidiagEquiv_symm_apply_apply, List.sym2_eq_sym_two, Sym.exists_cons_of_mem, Finset.sym_mono, Sym.exists_eq_cons_of_succ, Sym.coe_attach, DividedPowers.dpow_finsupp_sum

---

← Back to Index