Multiset

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

Statistics

Metric	Count
Definitions `instWellFoundedRelationNat`, `orderIsoMultiset`, `toMultiset`, `toFinsupp`, `equivNatSum`, `equivNatSumOfFintype`	6
Theorems `card_toMultiset`, `coe_orderIsoMultiset`, `coe_orderIsoMultiset_symm`, `count_toMultiset`, `lt_wf`, `mem_toMultiset`, `prod_toMultiset`, `sum_id_lt_of_lt`, `sum_toMultiset`, `toFinset_toMultiset`, `toMultiset_add`, `toMultiset_apply`, `toMultiset_eq_iff`, `toMultiset_inf`, `toMultiset_map`, `toMultiset_single`, `toMultiset_strictMono`, `toMultiset_sum`, `toMultiset_sum_single`, `toMultiset_sup`, `toMultiset_toFinsupp`, `toMultiset_zero`, `toFinsupp_add`, `toFinsupp_apply`, `toFinsupp_eq_iff`, `toFinsupp_inter`, `toFinsupp_singleton`, `toFinsupp_strictMono`, `toFinsupp_sum_eq`, `toFinsupp_support`, `toFinsupp_symm_apply`, `toFinsupp_toMultiset`, `toFinsupp_union`, `toFinsupp_zero`, `coe_equivNatSumOfFintype_apply_apply`, `coe_equivNatSumOfFintype_symm_apply`, `coe_equivNatSum_apply_apply`, `coe_equivNatSum_symm_apply`	38
Total	44

Finsupp

Definitions

Name	Category	Theorems
`instWellFoundedRelationNat` 📖	CompOp	—
`orderIsoMultiset` 📖	CompOp	2 math math: `coe_orderIsoMultiset_symm`, `coe_orderIsoMultiset`
`toMultiset` 📖	CompOp	27 math math: `sum_toMultiset`, `MvPolynomial.degrees_monomial`, `toMultiset_strictMono`, `prod_toMultiset`, `toMultiset_zero`, `toMultiset_toFinsupp`, `MvPolynomial.totalDegree_eq`, `MvPolynomial.degrees_def`, `card_toMultiset`, `Sym.coe_equivNatSum_symm_apply`, `toMultiset_apply`, `mem_toMultiset`, `count_toMultiset`, `toMultiset_add`, `Multiset.toFinsupp_symm_apply`, `Multiset.toFinsupp_toMultiset`, `toFinset_toMultiset`, `Multiset.toFinsupp_eq_iff`, `toMultiset_sum`, `MvPolynomial.degrees_monomial_eq`, `toMultiset_single`, `toMultiset_sup`, `toMultiset_sum_single`, `toMultiset_map`, `toMultiset_inf`, `coe_orderIsoMultiset`, `toMultiset_eq_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_toMultiset` 📖	mathematical	—	`Multiset.card` `DFunLike.coe` `AddMonoidHom` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Multiset` `AddZeroClass.toAddZero` `instAddZeroClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddCommMonoid.toAddMonoid` `AddCancelCommMonoid.toAddCommMonoid` `Multiset.instAddCancelCommMonoid` `AddMonoidHom.instFunLike` `toMultiset` `sum` `Nat.instAddCommMonoid`	—	`Multiset.card_finsuppSum` `Multiset.card_nsmul` `Multiset.card_singleton` `mul_one`
`coe_orderIsoMultiset` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Multiset` `instLE` `Preorder.toLE` `PartialOrder.toPreorder` `Multiset.instPartialOrder` `instFunLikeOrderIso` `orderIsoMultiset` `AddMonoidHom` `AddZeroClass.toAddZero` `instAddZeroClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddCommMonoid.toAddMonoid` `AddCancelCommMonoid.toAddCommMonoid` `Multiset.instAddCancelCommMonoid` `AddMonoidHom.instFunLike` `toMultiset`	—	—
`coe_orderIsoMultiset_symm` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `Multiset` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Preorder.toLE` `PartialOrder.toPreorder` `Multiset.instPartialOrder` `instLE` `instFunLikeOrderIso` `OrderIso.symm` `orderIsoMultiset` `AddEquiv` `Multiset.instAdd` `instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `Multiset.toFinsupp`	—	—
`count_toMultiset` 📖	mathematical	—	`Multiset.count` `DFunLike.coe` `AddMonoidHom` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Multiset` `AddZeroClass.toAddZero` `instAddZeroClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddCommMonoid.toAddMonoid` `AddCancelCommMonoid.toAddCommMonoid` `Multiset.instAddCancelCommMonoid` `AddMonoidHom.instFunLike` `toMultiset` `instFunLike`	—	`toMultiset_apply` `map_sum` `AddMonoidHom.instAddMonoidHomClass` `Multiset.count_nsmul` `sum_eq_single` `Multiset.count_singleton` `MulZeroClass.mul_zero` `MulZeroClass.zero_mul` `Multiset.count_singleton_self` `mul_one`
`lt_wf` 📖	mathematical	—	`Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Preorder.toLT` `preorder` `Nat.instPreorder`	—	`sum_id_lt_of_lt`
`mem_toMultiset` 📖	mathematical	—	`Multiset` `Multiset.instMembership` `DFunLike.coe` `AddMonoidHom` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `AddZeroClass.toAddZero` `instAddZeroClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddCommMonoid.toAddMonoid` `AddCancelCommMonoid.toAddCommMonoid` `Multiset.instAddCancelCommMonoid` `AddMonoidHom.instFunLike` `toMultiset` `Finset` `Finset.instMembership` `support`	—	`Multiset.count_ne_zero` `count_toMultiset` `mem_support_iff`
`prod_toMultiset` 📖	mathematical	—	`Multiset.prod` `DFunLike.coe` `AddMonoidHom` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Multiset` `AddZeroClass.toAddZero` `instAddZeroClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddCommMonoid.toAddMonoid` `AddCancelCommMonoid.toAddCommMonoid` `Multiset.instAddCancelCommMonoid` `AddMonoidHom.instFunLike` `toMultiset` `prod` `Monoid.toNatPow` `CommMonoid.toMonoid`	—	`induction` `toMultiset_zero` `Multiset.prod_zero` `prod_zero_index` `toMultiset_add` `Multiset.prod_add` `toMultiset_single` `Multiset.prod_nsmul` `prod_add_index'` `pow_zero` `pow_add` `prod_single_index` `Multiset.prod_singleton`
`sum_id_lt_of_lt` 📖	mathematical	`Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Preorder.toLT` `preorder` `Nat.instPreorder`	`sum` `Nat.instAddCommMonoid`	—	`card_toMultiset` `Multiset.card_lt_card` `toMultiset_strictMono`
`sum_toMultiset` 📖	mathematical	—	`Multiset.sum` `DFunLike.coe` `AddMonoidHom` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Multiset` `AddZeroClass.toAddZero` `instAddZeroClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddCommMonoid.toAddMonoid` `AddCancelCommMonoid.toAddCommMonoid` `Multiset.instAddCancelCommMonoid` `AddMonoidHom.instFunLike` `toMultiset` `sum` `AddMonoid.toNatSMul`	—	`induction` `toMultiset_zero` `Multiset.sum_zero` `sum_zero_index` `toMultiset_add` `Multiset.sum_add` `toMultiset_single` `Multiset.sum_nsmul` `sum_add_index'` `zero_nsmul` `add_nsmul` `sum_single_index` `Multiset.sum_singleton`
`toFinset_toMultiset` 📖	mathematical	—	`Multiset.toFinset` `DFunLike.coe` `AddMonoidHom` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Multiset` `AddZeroClass.toAddZero` `instAddZeroClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddCommMonoid.toAddMonoid` `AddCancelCommMonoid.toAddCommMonoid` `Multiset.instAddCancelCommMonoid` `AddMonoidHom.instFunLike` `toMultiset` `support`	—	`induction` `toMultiset_zero` `Multiset.toFinset_zero` `support_zero` `toMultiset_add` `Multiset.toFinset_add` `toMultiset_single` `support_add_eq` `Disjoint.mono_left` `support_single_subset` `Finset.disjoint_singleton_left` `support_single_ne_zero` `Multiset.toFinset_nsmul` `Multiset.toFinset_singleton`
`toMultiset_add` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Multiset` `AddZeroClass.toAddZero` `instAddZeroClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddCommMonoid.toAddMonoid` `AddCancelCommMonoid.toAddCommMonoid` `Multiset.instAddCancelCommMonoid` `AddMonoidHom.instFunLike` `toMultiset` `instAdd` `Multiset.instAdd`	—	`AddMonoidHom.map_add`
`toMultiset_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Multiset` `AddZeroClass.toAddZero` `instAddZeroClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddCommMonoid.toAddMonoid` `AddCancelCommMonoid.toAddCommMonoid` `Multiset.instAddCancelCommMonoid` `AddMonoidHom.instFunLike` `toMultiset` `sum` `AddMonoid.toNatSMul` `Multiset.instSingleton`	—	—
`toMultiset_eq_iff` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Multiset` `AddZeroClass.toAddZero` `instAddZeroClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddCommMonoid.toAddMonoid` `AddCancelCommMonoid.toAddCommMonoid` `Multiset.instAddCancelCommMonoid` `AddMonoidHom.instFunLike` `toMultiset` `AddEquiv` `Multiset.instAdd` `instAdd` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `Multiset.toFinsupp`	—	`AddEquiv.symm_apply_eq`
`toMultiset_inf` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Multiset` `AddZeroClass.toAddZero` `instAddZeroClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddCommMonoid.toAddMonoid` `AddCancelCommMonoid.toAddCommMonoid` `Multiset.instAddCancelCommMonoid` `AddMonoidHom.instFunLike` `toMultiset` `SemilatticeInf.toMin` `semilatticeInf` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeNat` `Multiset.instInter`	—	`Multiset.ext'` `Multiset.count_inter` `count_toMultiset`
`toMultiset_map` 📖	mathematical	—	`Multiset.map` `DFunLike.coe` `AddMonoidHom` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Multiset` `AddZeroClass.toAddZero` `instAddZeroClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddCommMonoid.toAddMonoid` `AddCancelCommMonoid.toAddCommMonoid` `Multiset.instAddCancelCommMonoid` `AddMonoidHom.instFunLike` `toMultiset` `mapDomain` `Nat.instAddCommMonoid`	—	`induction` `toMultiset_zero` `Multiset.map_zero` `mapDomain_zero` `toMultiset_add` `Multiset.map_add` `mapDomain_add` `mapDomain_single` `toMultiset_single` `Multiset.coe_mapAddMonoidHom` `AddMonoidHom.map_nsmul`
`toMultiset_single` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Multiset` `AddZeroClass.toAddZero` `instAddZeroClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddCommMonoid.toAddMonoid` `AddCancelCommMonoid.toAddCommMonoid` `Multiset.instAddCancelCommMonoid` `AddMonoidHom.instFunLike` `toMultiset` `single` `AddMonoid.toNatSMul` `Multiset.instSingleton`	—	`toMultiset_apply` `sum_single_index` `zero_nsmul`
`toMultiset_strictMono` 📖	mathematical	—	`StrictMono` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Multiset` `preorder` `Nat.instPreorder` `PartialOrder.toPreorder` `Multiset.instPartialOrder` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `instAddZeroClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddCommMonoid.toAddMonoid` `AddCancelCommMonoid.toAddCommMonoid` `Multiset.instAddCancelCommMonoid` `AddMonoidHom.instFunLike` `toMultiset`	—	`OrderIso.strictMono`
`toMultiset_sum` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Multiset` `AddZeroClass.toAddZero` `instAddZeroClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddCommMonoid.toAddMonoid` `AddCancelCommMonoid.toAddCommMonoid` `Multiset.instAddCancelCommMonoid` `AddMonoidHom.instFunLike` `toMultiset` `Finset.sum` `instAddCommMonoid` `Nat.instAddCommMonoid`	—	`map_sum` `AddMonoidHom.instAddMonoidHomClass`
`toMultiset_sum_single` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Multiset` `AddZeroClass.toAddZero` `instAddZeroClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddCommMonoid.toAddMonoid` `AddCancelCommMonoid.toAddCommMonoid` `Multiset.instAddCancelCommMonoid` `AddMonoidHom.instFunLike` `toMultiset` `Finset.sum` `instAddCommMonoid` `Nat.instAddCommMonoid` `single` `AddMonoid.toNatSMul` `Finset.val`	—	`toMultiset_sum` `Finset.sum_congr` `toMultiset_single` `Finset.sum_nsmul` `Finset.sum_multiset_singleton`
`toMultiset_sup` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Multiset` `AddZeroClass.toAddZero` `instAddZeroClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddCommMonoid.toAddMonoid` `AddCancelCommMonoid.toAddCommMonoid` `Multiset.instAddCancelCommMonoid` `AddMonoidHom.instFunLike` `toMultiset` `SemilatticeSup.toMax` `semilatticeSup` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `instDistribLatticeNat` `Multiset.instUnion`	—	`Multiset.ext'` `Multiset.count_union` `count_toMultiset`
`toMultiset_toFinsupp` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `Multiset` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Multiset.instAdd` `instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `Multiset.toFinsupp` `AddMonoidHom` `AddZeroClass.toAddZero` `instAddZeroClass` `AddCommMonoid.toAddMonoid` `AddCancelCommMonoid.toAddCommMonoid` `Multiset.instAddCancelCommMonoid` `AddMonoidHom.instFunLike` `toMultiset`	—	`AddEquiv.apply_symm_apply`
`toMultiset_zero` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Multiset` `AddZeroClass.toAddZero` `instAddZeroClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddCommMonoid.toAddMonoid` `AddCancelCommMonoid.toAddCommMonoid` `Multiset.instAddCancelCommMonoid` `AddMonoidHom.instFunLike` `toMultiset` `instZero` `Multiset.instZero`	—	—

Multiset

Definitions

Name	Category	Theorems
`toFinsupp` 📖	CompOp	18 math math: `toFinsupp_add`, `Finsupp.toMultiset_toFinsupp`, `toFinsupp_sum_eq`, `toFinsupp_union`, `toFinsupp_inter`, `toFinsupp_apply`, `Relation.cutExpand_le_invImage_lex`, `toFinsupp_singleton`, `toFinsupp_symm_apply`, `Finsupp.coe_orderIsoMultiset_symm`, `toFinsupp_zero`, `toFinsupp_toMultiset`, `Nat.factorization_eq_primeFactorsList_multiset`, `toFinsupp_eq_iff`, `Nat.Partition.coeff_genFun`, `toFinsupp_support`, `toFinsupp_strictMono`, `Finsupp.toMultiset_eq_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toFinsupp_add` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `Multiset` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instAdd` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `toFinsupp`	—	`map_add` `AddMonoidHomClass.toAddHomClass` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass`
`toFinsupp_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instFunLike` `AddEquiv` `Multiset` `instAdd` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `toFinsupp` `count`	—	—
`toFinsupp_eq_iff` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `Multiset` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instAdd` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `toFinsupp` `AddMonoidHom` `AddZeroClass.toAddZero` `Finsupp.instAddZeroClass` `AddCommMonoid.toAddMonoid` `AddCancelCommMonoid.toAddCommMonoid` `instAddCancelCommMonoid` `AddMonoidHom.instFunLike` `Finsupp.toMultiset`	—	`AddEquiv.apply_eq_iff_symm_apply`
`toFinsupp_inter` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `Multiset` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instAdd` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `toFinsupp` `instInter` `SemilatticeInf.toMin` `Finsupp.semilatticeInf` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeNat`	—	`Finsupp.ext` `count_inter`
`toFinsupp_singleton` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `Multiset` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instAdd` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `toFinsupp` `instSingleton` `Finsupp.single`	—	`Finsupp.ext` `toFinsupp_apply` `count_singleton` `Finsupp.single_eq_pi_single` `Pi.single_apply`
`toFinsupp_strictMono` 📖	mathematical	—	`StrictMono` `Multiset` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `PartialOrder.toPreorder` `instPartialOrder` `Finsupp.preorder` `Nat.instPreorder` `DFunLike.coe` `AddEquiv` `instAdd` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `toFinsupp`	—	`OrderIso.strictMono`
`toFinsupp_sum_eq` 📖	mathematical	—	`Finsupp.sum` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Nat.instAddCommMonoid` `DFunLike.coe` `AddEquiv` `Multiset` `Finsupp` `instAdd` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `toFinsupp` `card`	—	`Finsupp.card_toMultiset` `toFinsupp_toMultiset`
`toFinsupp_support` 📖	mathematical	—	`Finsupp.support` `MulZeroClass.toZero` `Nat.instMulZeroClass` `DFunLike.coe` `AddEquiv` `Multiset` `Finsupp` `instAdd` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `toFinsupp` `toFinset`	—	—
`toFinsupp_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Multiset` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `instAdd` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm` `toFinsupp` `AddMonoidHom` `AddZeroClass.toAddZero` `Finsupp.instAddZeroClass` `AddCommMonoid.toAddMonoid` `AddCancelCommMonoid.toAddCommMonoid` `instAddCancelCommMonoid` `AddMonoidHom.instFunLike` `Finsupp.toMultiset`	—	—
`toFinsupp_toMultiset` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Multiset` `AddZeroClass.toAddZero` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddCommMonoid.toAddMonoid` `AddCancelCommMonoid.toAddCommMonoid` `instAddCancelCommMonoid` `AddMonoidHom.instFunLike` `Finsupp.toMultiset` `AddEquiv` `instAdd` `Finsupp.instAdd` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `toFinsupp`	—	`AddEquiv.symm_apply_apply`
`toFinsupp_union` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `Multiset` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instAdd` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `toFinsupp` `instUnion` `SemilatticeSup.toMax` `Finsupp.semilatticeSup` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `instDistribLatticeNat`	—	`Finsupp.ext` `count_union`
`toFinsupp_zero` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `Multiset` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instAdd` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `toFinsupp` `instZero` `Finsupp.instZero`	—	`map_zero` `AddMonoidHomClass.toZeroHomClass` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass`

Sym

Definitions

Name	Category	Theorems
`equivNatSum` 📖	CompOp	2 math math: `coe_equivNatSum_apply_apply`, `coe_equivNatSum_symm_apply`
`equivNatSumOfFintype` 📖	CompOp	2 math math: `coe_equivNatSumOfFintype_apply_apply`, `coe_equivNatSumOfFintype_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_equivNatSumOfFintype_apply_apply` 📖	mathematical	—	`Finset.sum` `Nat.instAddCommMonoid` `Finset.univ` `DFunLike.coe` `Equiv` `Sym` `EquivLike.toFunLike` `Equiv.instEquivLike` `equivNatSumOfFintype` `Multiset.count` `toMultiset`	—	—
`coe_equivNatSumOfFintype_symm_apply` 📖	mathematical	—	`toMultiset` `DFunLike.coe` `Equiv` `Finset.sum` `Nat.instAddCommMonoid` `Finset.univ` `Sym` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equivNatSumOfFintype` `Multiset` `AddCancelCommMonoid.toAddCommMonoid` `Multiset.instAddCancelCommMonoid` `AddMonoid.toNatSMul` `AddCommMonoid.toAddMonoid` `Multiset.instSingleton`	—	`Multiset.ext'` `Finite.of_fintype` `Multiset.count_sum` `Finsupp.count_toMultiset` `Multiset.map_congr` `Multiset.count_nsmul` `Multiset.count_singleton` `mul_ite` `mul_one` `MulZeroClass.mul_zero` `Finset.sum_ite_eq`
`coe_equivNatSum_apply_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instFunLike` `Finsupp.sum` `Nat.instAddCommMonoid` `Equiv` `Sym` `EquivLike.toFunLike` `Equiv.instEquivLike` `equivNatSum` `Multiset.count` `toMultiset`	—	—
`coe_equivNatSum_symm_apply` 📖	mathematical	—	`toMultiset` `DFunLike.coe` `Equiv` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.sum` `Nat.instAddCommMonoid` `Sym` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equivNatSum` `AddMonoidHom` `Multiset` `AddZeroClass.toAddZero` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddCommMonoid.toAddMonoid` `AddCancelCommMonoid.toAddCommMonoid` `Multiset.instAddCancelCommMonoid` `AddMonoidHom.instFunLike` `Finsupp.toMultiset`	—	—

---

← Back to Index