Multiset

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

Statistics

Metric	Count
Definitions addZeroClass', toMultiset, equivDFinsupp, toDFinsupp	4
Theorems toMultiset_inf, toMultiset_inj, toMultiset_injective, toMultiset_le_toMultiset, toMultiset_lt_toMultiset, toMultiset_single, toMultiset_sup, toMultiset_toDFinsupp, equivDFinsupp_apply, equivDFinsupp_symm_apply, toDFinsupp_apply, toDFinsupp_inj, toDFinsupp_injective, toDFinsupp_inter, toDFinsupp_le_toDFinsupp, toDFinsupp_lt_toDFinsupp, toDFinsupp_replicate, toDFinsupp_singleton, toDFinsupp_support, toDFinsupp_toMultiset, toDFinsupp_union	21
Total	25

DFinsupp

Definitions

Name	Category	Theorems
addZeroClass' 📖	CompOp	23 math math: toMultiset_sup, Multiset.equivDFinsupp_symm_apply, Multiset.toDFinsupp_support, Multiset.Icc_eq, Multiset.toDFinsupp_apply, Multiset.equivDFinsupp_apply, toMultiset_single, toMultiset_le_toMultiset, Multiset.toDFinsupp_replicate, Multiset.uIcc_eq, toMultiset_toDFinsupp, toMultiset_inf, toMultiset_injective, Multiset.toDFinsupp_injective, Multiset.toDFinsupp_le_toDFinsupp, Multiset.toDFinsupp_toMultiset, Multiset.toDFinsupp_singleton, Multiset.toDFinsupp_inter, Multiset.toDFinsupp_lt_toDFinsupp, Multiset.toDFinsupp_union, toMultiset_inj, toMultiset_lt_toMultiset, Multiset.toDFinsupp_inj
toMultiset 📖	CompOp	10 math math: toMultiset_sup, Multiset.equivDFinsupp_symm_apply, toMultiset_single, toMultiset_le_toMultiset, toMultiset_toDFinsupp, toMultiset_inf, toMultiset_injective, Multiset.toDFinsupp_toMultiset, toMultiset_inj, toMultiset_lt_toMultiset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toMultiset_inf 📖	mathematical	—	DFunLike.coe AddMonoidHom DFinsupp MulZeroClass.toZero Nat.instMulZeroClass Multiset AddZeroClass.toAddZero addZeroClass' AddMonoid.toAddZeroClass Nat.instAddMonoid AddCommMonoid.toAddMonoid AddCancelCommMonoid.toAddCommMonoid Multiset.instAddCancelCommMonoid AddMonoidHom.instFunLike toMultiset SemilatticeInf.toMin instSemilatticeInf Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeNat Multiset.instInter	—	Multiset.toDFinsupp_injective toMultiset_toDFinsupp Multiset.toDFinsupp_inter
toMultiset_inj 📖	mathematical	—	DFunLike.coe AddMonoidHom DFinsupp MulZeroClass.toZero Nat.instMulZeroClass Multiset AddZeroClass.toAddZero addZeroClass' AddMonoid.toAddZeroClass Nat.instAddMonoid AddCommMonoid.toAddMonoid AddCancelCommMonoid.toAddCommMonoid Multiset.instAddCancelCommMonoid AddMonoidHom.instFunLike toMultiset	—	toMultiset_injective
toMultiset_injective 📖	mathematical	—	DFinsupp MulZeroClass.toZero Nat.instMulZeroClass Multiset DFunLike.coe AddMonoidHom AddZeroClass.toAddZero addZeroClass' AddMonoid.toAddZeroClass Nat.instAddMonoid AddCommMonoid.toAddMonoid AddCancelCommMonoid.toAddCommMonoid Multiset.instAddCancelCommMonoid AddMonoidHom.instFunLike toMultiset	—	AddEquiv.injective
toMultiset_le_toMultiset 📖	mathematical	—	Multiset Preorder.toLE PartialOrder.toPreorder Multiset.instPartialOrder DFunLike.coe AddMonoidHom DFinsupp MulZeroClass.toZero Nat.instMulZeroClass AddZeroClass.toAddZero addZeroClass' AddMonoid.toAddZeroClass Nat.instAddMonoid AddCommMonoid.toAddMonoid AddCancelCommMonoid.toAddCommMonoid Multiset.instAddCancelCommMonoid AddMonoidHom.instFunLike toMultiset instLE	—	toMultiset_toDFinsupp
toMultiset_lt_toMultiset 📖	mathematical	—	Multiset Preorder.toLT PartialOrder.toPreorder Multiset.instPartialOrder DFunLike.coe AddMonoidHom DFinsupp MulZeroClass.toZero Nat.instMulZeroClass AddZeroClass.toAddZero addZeroClass' AddMonoid.toAddZeroClass Nat.instAddMonoid AddCommMonoid.toAddMonoid AddCancelCommMonoid.toAddCommMonoid Multiset.instAddCancelCommMonoid AddMonoidHom.instFunLike toMultiset instPreorder Nat.instPreorder	—	toMultiset_toDFinsupp
toMultiset_single 📖	mathematical	—	DFunLike.coe AddMonoidHom DFinsupp MulZeroClass.toZero Nat.instMulZeroClass Multiset AddZeroClass.toAddZero addZeroClass' AddMonoid.toAddZeroClass Nat.instAddMonoid AddCommMonoid.toAddMonoid AddCancelCommMonoid.toAddCommMonoid Multiset.instAddCancelCommMonoid AddMonoidHom.instFunLike toMultiset single Multiset.replicate	—	sumAddHom_single
toMultiset_sup 📖	mathematical	—	DFunLike.coe AddMonoidHom DFinsupp MulZeroClass.toZero Nat.instMulZeroClass Multiset AddZeroClass.toAddZero addZeroClass' AddMonoid.toAddZeroClass Nat.instAddMonoid AddCommMonoid.toAddMonoid AddCancelCommMonoid.toAddCommMonoid Multiset.instAddCancelCommMonoid AddMonoidHom.instFunLike toMultiset SemilatticeSup.toMax instSemilatticeSup Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeNat Multiset.instUnion	—	Multiset.toDFinsupp_injective toMultiset_toDFinsupp Multiset.toDFinsupp_union
toMultiset_toDFinsupp 📖	mathematical	—	DFunLike.coe AddMonoidHom Multiset DFinsupp MulZeroClass.toZero Nat.instMulZeroClass AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddCancelCommMonoid.toAddCommMonoid Multiset.instAddCancelCommMonoid addZeroClass' Nat.instAddMonoid AddMonoidHom.instFunLike Multiset.toDFinsupp toMultiset	—	AddEquiv.apply_symm_apply

Multiset

Definitions

Name	Category	Theorems
equivDFinsupp 📖	CompOp	4 math math: equivDFinsupp_symm_apply, Icc_eq, equivDFinsupp_apply, uIcc_eq
toDFinsupp 📖	CompOp	15 math math: toDFinsupp_support, Icc_eq, toDFinsupp_apply, equivDFinsupp_apply, toDFinsupp_replicate, uIcc_eq, DFinsupp.toMultiset_toDFinsupp, toDFinsupp_injective, toDFinsupp_le_toDFinsupp, toDFinsupp_toMultiset, toDFinsupp_singleton, toDFinsupp_inter, toDFinsupp_lt_toDFinsupp, toDFinsupp_union, toDFinsupp_inj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
equivDFinsupp_apply 📖	mathematical	—	DFunLike.coe AddEquiv Multiset DFinsupp MulZeroClass.toZero Nat.instMulZeroClass instAdd DFinsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid EquivLike.toFunLike AddEquiv.instEquivLike equivDFinsupp AddMonoidHom AddZeroClass.toAddZero AddCommMonoid.toAddMonoid AddCancelCommMonoid.toAddCommMonoid instAddCancelCommMonoid DFinsupp.addZeroClass' AddMonoidHom.instFunLike toDFinsupp	—	—
equivDFinsupp_symm_apply 📖	mathematical	—	DFunLike.coe AddEquiv DFinsupp MulZeroClass.toZero Nat.instMulZeroClass Multiset DFinsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid instAdd EquivLike.toFunLike AddEquiv.instEquivLike AddEquiv.symm equivDFinsupp AddMonoidHom AddZeroClass.toAddZero DFinsupp.addZeroClass' AddCommMonoid.toAddMonoid AddCancelCommMonoid.toAddCommMonoid instAddCancelCommMonoid AddMonoidHom.instFunLike DFinsupp.toMultiset	—	—
toDFinsupp_apply 📖	mathematical	—	DFunLike.coe DFinsupp MulZeroClass.toZero Nat.instMulZeroClass DFinsupp.instDFunLike AddMonoidHom Multiset AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddCancelCommMonoid.toAddCommMonoid instAddCancelCommMonoid DFinsupp.addZeroClass' Nat.instAddMonoid AddMonoidHom.instFunLike toDFinsupp count	—	—
toDFinsupp_inj 📖	mathematical	—	DFunLike.coe AddMonoidHom Multiset DFinsupp MulZeroClass.toZero Nat.instMulZeroClass AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddCancelCommMonoid.toAddCommMonoid instAddCancelCommMonoid DFinsupp.addZeroClass' Nat.instAddMonoid AddMonoidHom.instFunLike toDFinsupp	—	toDFinsupp_injective
toDFinsupp_injective 📖	mathematical	—	Multiset DFinsupp MulZeroClass.toZero Nat.instMulZeroClass DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddCancelCommMonoid.toAddCommMonoid instAddCancelCommMonoid DFinsupp.addZeroClass' Nat.instAddMonoid AddMonoidHom.instFunLike toDFinsupp	—	AddEquiv.injective
toDFinsupp_inter 📖	mathematical	—	DFunLike.coe AddMonoidHom Multiset DFinsupp MulZeroClass.toZero Nat.instMulZeroClass AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddCancelCommMonoid.toAddCommMonoid instAddCancelCommMonoid DFinsupp.addZeroClass' Nat.instAddMonoid AddMonoidHom.instFunLike toDFinsupp instInter SemilatticeInf.toMin DFinsupp.instSemilatticeInf Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeNat	—	DFinsupp.ext count_inter
toDFinsupp_le_toDFinsupp 📖	mathematical	—	DFinsupp MulZeroClass.toZero Nat.instMulZeroClass DFinsupp.instLE DFunLike.coe AddMonoidHom Multiset AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddCancelCommMonoid.toAddCommMonoid instAddCancelCommMonoid DFinsupp.addZeroClass' Nat.instAddMonoid AddMonoidHom.instFunLike toDFinsupp Preorder.toLE PartialOrder.toPreorder instPartialOrder	—	—
toDFinsupp_lt_toDFinsupp 📖	mathematical	—	DFinsupp MulZeroClass.toZero Nat.instMulZeroClass Preorder.toLT DFinsupp.instPreorder Nat.instPreorder DFunLike.coe AddMonoidHom Multiset AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddCancelCommMonoid.toAddCommMonoid instAddCancelCommMonoid DFinsupp.addZeroClass' Nat.instAddMonoid AddMonoidHom.instFunLike toDFinsupp PartialOrder.toPreorder instPartialOrder	—	lt_iff_lt_of_le_iff_le' toDFinsupp_le_toDFinsupp
toDFinsupp_replicate 📖	mathematical	—	DFunLike.coe AddMonoidHom Multiset DFinsupp MulZeroClass.toZero Nat.instMulZeroClass AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddCancelCommMonoid.toAddCommMonoid instAddCancelCommMonoid DFinsupp.addZeroClass' Nat.instAddMonoid AddMonoidHom.instFunLike toDFinsupp replicate DFinsupp.single	—	DFinsupp.ext count_replicate DFinsupp.single_apply
toDFinsupp_singleton 📖	mathematical	—	DFunLike.coe AddMonoidHom Multiset DFinsupp MulZeroClass.toZero Nat.instMulZeroClass AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddCancelCommMonoid.toAddCommMonoid instAddCancelCommMonoid DFinsupp.addZeroClass' Nat.instAddMonoid AddMonoidHom.instFunLike toDFinsupp instSingleton DFinsupp.single	—	replicate_one toDFinsupp_replicate
toDFinsupp_support 📖	mathematical	—	DFinsupp.support MulZeroClass.toZero Nat.instMulZeroClass DFunLike.coe AddMonoidHom Multiset DFinsupp AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddCancelCommMonoid.toAddCommMonoid instAddCancelCommMonoid DFinsupp.addZeroClass' Nat.instAddMonoid AddMonoidHom.instFunLike toDFinsupp toFinset	—	Finset.filter_true_of_mem count_ne_zero mem_toFinset
toDFinsupp_toMultiset 📖	mathematical	—	DFunLike.coe AddMonoidHom DFinsupp MulZeroClass.toZero Nat.instMulZeroClass Multiset AddZeroClass.toAddZero DFinsupp.addZeroClass' AddMonoid.toAddZeroClass Nat.instAddMonoid AddCommMonoid.toAddMonoid AddCancelCommMonoid.toAddCommMonoid instAddCancelCommMonoid AddMonoidHom.instFunLike DFinsupp.toMultiset toDFinsupp	—	AddEquiv.symm_apply_apply
toDFinsupp_union 📖	mathematical	—	DFunLike.coe AddMonoidHom Multiset DFinsupp MulZeroClass.toZero Nat.instMulZeroClass AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddCancelCommMonoid.toAddCommMonoid instAddCancelCommMonoid DFinsupp.addZeroClass' Nat.instAddMonoid AddMonoidHom.instFunLike toDFinsupp instUnion SemilatticeSup.toMax DFinsupp.instSemilatticeSup Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeNat	—	DFinsupp.ext count_union

---

← Back to Index