NoncommProd

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

Statistics

Metric	Count
Definitions `noncommProd`, `noncommSum`, `noncommFold`, `noncommFoldr`, `noncommProd`, `noncommSum`	6
Theorems `pi_ext`, `map_noncommProd`, `map_noncommSum`, `mul_noncommProd_erase`, `noncommProd_commute`, `noncommProd_congr`, `noncommProd_cons`, `noncommProd_cons'`, `noncommProd_empty`, `noncommProd_eq_pow_card`, `noncommProd_eq_prod`, `noncommProd_erase_mul`, `noncommProd_induction`, `noncommProd_insert_of_notMem`, `noncommProd_insert_of_notMem'`, `noncommProd_lemma`, `noncommProd_mulSingle`, `noncommProd_mul_distrib`, `noncommProd_mul_distrib_aux`, `noncommProd_mul_single`, `noncommProd_singleton`, `noncommProd_toFinset`, `noncommProd_union_of_disjoint`, `noncommSum_addCommute`, `noncommSum_add_distrib`, `noncommSum_add_distrib_aux`, `noncommSum_add_single`, `noncommSum_congr`, `noncommSum_cons`, `noncommSum_cons'`, `noncommSum_empty`, `noncommSum_eq_card_nsmul`, `noncommSum_eq_sum`, `noncommSum_induction`, `noncommSum_insert_of_notMem`, `noncommSum_insert_of_notMem'`, `noncommSum_lemma`, `noncommSum_single`, `noncommSum_singleton`, `noncommSum_toFinset`, `noncommSum_union_of_disjoint`, `pi_ext`, `map_noncommProd`, `map_noncommProd_aux`, `map_noncommSum`, `map_noncommSum_aux`, `mul_noncommProd_erase`, `noncommFold_coe`, `noncommFold_cons`, `noncommFold_empty`, `noncommFold_eq_fold`, `noncommFoldr_coe`, `noncommFoldr_cons`, `noncommFoldr_empty`, `noncommFoldr_eq_foldr`, `noncommProd_add`, `noncommProd_coe`, `noncommProd_commute`, `noncommProd_cons`, `noncommProd_cons'`, `noncommProd_empty`, `noncommProd_eq_pow_card`, `noncommProd_eq_prod`, `noncommProd_erase_mul`, `noncommProd_induction`, `noncommSum_add`, `noncommSum_addCommute`, `noncommSum_coe`, `noncommSum_cons`, `noncommSum_cons'`, `noncommSum_empty`, `noncommSum_eq_card_nsmul`, `noncommSum_eq_sum`, `noncommSum_induction`	74
Total	80

AddMonoidHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`pi_ext` 📖	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `Pi.addZeroClass` `AddMonoid.toAddZeroClass` `instFunLike` `Pi.single` `AddZero.toZero`	—	—	`nonempty_fintype` `ext` `Pi.single_apply_addCommute` `Finset.noncommSum_single` `AddCommute.map` `AddMonoidHomClass.toAddHomClass` `instAddMonoidHomClass` `Set.Pairwise.of_refl` `AddCommute.on_refl` `Finset.map_noncommSum`

Finset

Definitions

Name	Category	Theorems
`noncommProd` 📖	CompOp	33 math math: `noncommProd_toFinset`, `Equiv.Perm.cycleFactorsFinset_noncommProd`, `noncommProd_eq_prod`, `Equiv.Perm.cycleFactorsFinset_eq_finset`, `noncommProd_union_of_disjoint`, `MonoidHom.noncommPiCoprod_apply`, `Subgroup.noncommPiCoprod_apply`, `noncommProd_induction`, `Equiv.Perm.support_noncommProd`, `Matrix.exp_sum_of_commute`, `LinearMap.ker_noncommProd_eq_of_supIndep_ker`, `noncommProd_erase_mul`, `noncommProd_mulSingle`, `noncommProd_mul_distrib`, `sum_pow_eq_sum_piAntidiag_of_commute`, `noncommProd_cons'`, `PiTensorProduct.tprod_noncommProd`, `Submonoid.noncommProd_mem`, `map_noncommProd`, `noncommProd_empty`, `noncommProd_mul_single`, `noncommProd_insert_of_notMem'`, `mul_noncommProd_erase`, `noncommProd_eq_pow_card`, `Equiv.Perm.Disjoint.cycleType_noncommProd`, `NormedSpace.exp_sum_of_commute`, `Equiv.Perm.disjoint_noncommProd_right`, `noncommProd_singleton`, `noncommProd_commute`, `Subgroup.noncommProd_mem`, `noncommProd_congr`, `noncommProd_insert_of_notMem`, `noncommProd_cons`
`noncommSum` 📖	CompOp	21 math math: `AddSubgroup.noncommSum_mem`, `noncommSum_singleton`, `AddMonoidHom.noncommPiCoprod_apply`, `noncommSum_union_of_disjoint`, `noncommSum_congr`, `AddSubgroup.noncommPiCoprod_apply`, `noncommSum_addCommute`, `noncommSum_single`, `AddSubmonoid.noncommSum_mem`, `noncommSum_eq_card_nsmul`, `noncommSum_insert_of_notMem`, `noncommSum_insert_of_notMem'`, `noncommSum_cons`, `noncommSum_induction`, `noncommSum_add_single`, `noncommSum_add_distrib`, `noncommSum_eq_sum`, `map_noncommSum`, `noncommSum_empty`, `noncommSum_cons'`, `noncommSum_toFinset`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_noncommProd` 📖	mathematical	`Set.Pairwise` `SetLike.coe` `Finset` `instSetLike` `Function.onFun` `Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`DFunLike.coe` `noncommProd` `Commute.map` `MonoidHomClass.toMulHomClass` `Set.Pairwise.of_refl` `Commute.on_refl`	—	`noncommProd_lemma` `Commute.map` `MonoidHomClass.toMulHomClass` `Set.Pairwise.of_refl` `Commute.on_refl` `Multiset.map_noncommProd_aux` `Multiset.map_map` `Multiset.map_congr` `Multiset.map_noncommProd` `Multiset.noncommProd.congr_simp`
`map_noncommSum` 📖	mathematical	`Set.Pairwise` `SetLike.coe` `Finset` `instSetLike` `Function.onFun` `AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`DFunLike.coe` `noncommSum` `AddCommute.map` `AddMonoidHomClass.toAddHomClass` `Set.Pairwise.of_refl` `AddCommute.on_refl`	—	`noncommSum_lemma` `AddCommute.map` `AddMonoidHomClass.toAddHomClass` `Set.Pairwise.of_refl` `AddCommute.on_refl` `Multiset.map_noncommSum_aux` `Multiset.map_map` `Multiset.map_congr` `Multiset.map_noncommSum` `Multiset.noncommSum.congr_simp`
`mul_noncommProd_erase` 📖	mathematical	`Finset` `instMembership` `Set.Pairwise` `SetLike.coe` `instSetLike` `Function.onFun` `Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `mem_of_mem_erase`	`noncommProd` `erase`	—	`noncommProd_lemma` `Multiset.mem_of_mem_erase` `Multiset.map_erase_of_mem` `Multiset.noncommProd.congr_simp` `Multiset.mul_noncommProd_erase` `Multiset.mem_map_of_mem`
`noncommProd_commute` 📖	mathematical	`Set.Pairwise` `SetLike.coe` `Finset` `instSetLike` `Function.onFun` `Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`noncommProd`	—	`Multiset.noncommProd_commute` `noncommProd_lemma` `Multiset.mem_map`
`noncommProd_congr` 📖	mathematical	`Set.Pairwise` `SetLike.coe` `Finset` `instSetLike` `Function.onFun` `Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`noncommProd`	—	`noncommProd_lemma` `Multiset.map_congr` `Multiset.noncommProd.congr_simp`
`noncommProd_cons` 📖	mathematical	`Finset` `instMembership` `Set.Pairwise` `SetLike.coe` `instSetLike` `cons` `Function.onFun` `Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`noncommProd` `Set.Pairwise.mono` `Multiset` `Multiset.instMembership` `val` `Set` `Set.instMembership` `mem_cons`	—	`Set.Pairwise.mono` `mem_cons` `noncommProd_lemma` `Multiset.map_cons` `Multiset.noncommProd.congr_simp` `Multiset.mem_cons_of_mem` `Multiset.noncommProd_cons`
`noncommProd_cons'` 📖	mathematical	`Finset` `instMembership` `Set.Pairwise` `SetLike.coe` `instSetLike` `cons` `Function.onFun` `Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`noncommProd` `Set.Pairwise.mono` `Multiset` `Multiset.instMembership` `val` `Set` `Set.instMembership` `mem_cons`	—	`Set.Pairwise.mono` `mem_cons` `noncommProd_lemma` `Multiset.map_cons` `Multiset.noncommProd.congr_simp` `Multiset.mem_cons_of_mem` `Multiset.noncommProd_cons'`
`noncommProd_empty` 📖	mathematical	`Set.Pairwise` `SetLike.coe` `Finset` `instSetLike` `instEmptyCollection` `Function.onFun` `Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`noncommProd` `MulOne.toOne`	—	—
`noncommProd_eq_pow_card` 📖	mathematical	`Set.Pairwise` `SetLike.coe` `Finset` `instSetLike` `Function.onFun` `Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`noncommProd` `Monoid.toNatPow` `card`	—	`noncommProd_lemma` `noncommProd.eq_1` `Multiset.noncommProd_eq_pow_card` `Multiset.card_map`
`noncommProd_eq_prod` 📖	mathematical	—	`noncommProd` `CommMonoid.toMonoid` `Commute.all` `CommSemigroup.toCommMagma` `CommMonoid.toCommSemigroup` `prod`	—	`cons_induction_on` `Commute.all` `Set.Pairwise.mono` `mem_cons` `noncommProd_cons` `prod_cons`
`noncommProd_erase_mul` 📖	mathematical	`Finset` `instMembership` `Set.Pairwise` `SetLike.coe` `instSetLike` `Function.onFun` `Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `mem_of_mem_erase`	`noncommProd` `erase`	—	`noncommProd_lemma` `Multiset.mem_of_mem_erase` `Multiset.map_erase_of_mem` `Multiset.noncommProd.congr_simp` `Multiset.noncommProd_erase_mul` `Multiset.mem_map_of_mem`
`noncommProd_induction` 📖	mathematical	`Set.Pairwise` `SetLike.coe` `Finset` `instSetLike` `Function.onFun` `Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne`	`noncommProd`	—	`Multiset.noncommProd_induction` `noncommProd_lemma`
`noncommProd_insert_of_notMem` 📖	mathematical	`Set.Pairwise` `SetLike.coe` `Finset` `instSetLike` `instInsert` `Function.onFun` `Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instMembership`	`noncommProd` `Set.Pairwise.mono` `Multiset` `Multiset.instMembership` `val` `mem_insert_of_mem`	—	`Set.Pairwise.mono` `mem_insert_of_mem` `mem_cons` `cons_eq_insert` `noncommProd_congr` `noncommProd_cons`
`noncommProd_insert_of_notMem'` 📖	mathematical	`Set.Pairwise` `SetLike.coe` `Finset` `instSetLike` `instInsert` `Function.onFun` `Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instMembership`	`noncommProd` `Set.Pairwise.mono` `Multiset` `Multiset.instMembership` `val` `mem_insert_of_mem`	—	`Set.Pairwise.mono` `mem_insert_of_mem` `mem_cons` `cons_eq_insert` `noncommProd_congr` `noncommProd_cons'`
`noncommProd_lemma` 📖	mathematical	`Set.Pairwise` `SetLike.coe` `Finset` `instSetLike` `Function.onFun` `Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`setOf` `Multiset` `Multiset.instMembership` `Multiset.map` `val`	—	`Multiset.map_set_pairwise`
`noncommProd_mulSingle` 📖	mathematical	—	`noncommProd` `Pi.monoid` `univ` `Pi.mulSingle` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Pi.mulSingle_apply_commute`	—	`Pi.mulSingle_apply_commute` `Commute.map` `MonoidHomClass.toMulHomClass` `MonoidHom.instMonoidHomClass` `Set.Pairwise.of_refl` `Commute.on_refl` `map_noncommProd` `insert_erase` `mem_univ` `noncommProd_congr` `Set.Pairwise.mono` `mem_insert_of_mem` `noncommProd_insert_of_notMem` `notMem_erase` `noncommProd_eq_pow_card` `one_pow` `mul_one` `Pi.mulSingle_eq_same`
`noncommProd_mul_distrib` 📖	mathematical	`Set.Pairwise` `SetLike.coe` `Finset` `instSetLike` `Function.onFun` `Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`noncommProd` `Pi.instMul` `noncommProd_mul_distrib_aux`	—	`cons_induction_on` `noncommProd_mul_distrib_aux` `noncommProd_congr` `mul_one` `Set.Pairwise.mono` `mem_cons` `noncommProd_cons` `Pi.mul_apply` `mem_cons_of_mem` `Commute.mul_mul_mul_comm` `noncommProd_commute` `mem_cons_self`
`noncommProd_mul_distrib_aux` 📖	mathematical	`Set.Pairwise` `SetLike.coe` `Finset` `instSetLike` `Function.onFun` `Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`Pi.instMul`	—	`Commute.mul_left` `Commute.mul_right` `Set.Pairwise.of_refl` `Commute.on_refl` `Commute.symm`
`noncommProd_mul_single` 📖	mathematical	—	`noncommProd` `Pi.monoid` `univ` `Pi.mulSingle` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Pi.mulSingle_apply_commute`	—	`noncommProd_mulSingle`
`noncommProd_singleton` 📖	mathematical	—	`noncommProd` `Finset` `instSingleton`	—	`mul_one`
`noncommProd_toFinset` 📖	mathematical	`Set.Pairwise` `SetLike.coe` `Finset` `instSetLike` `List.toFinset` `Function.onFun` `Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`noncommProd` `MulOne.toOne`	—	`noncommProd_lemma` `Multiset.map_congr` `List.dedup_eq_self` `Multiset.noncommProd.congr_simp` `Multiset.noncommProd_coe`
`noncommProd_union_of_disjoint` 📖	mathematical	`Disjoint` `Finset` `partialOrder` `instOrderBot` `Set.Pairwise` `setOf` `instMembership` `instUnion` `Function.onFun` `Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`noncommProd` `Set.Pairwise.mono` `SetLike.coe` `instSetLike` `Set` `Set.instHasSubset` `instHasSubset` `coe_subset` `subset_union_left` `subset_union_right`	—	`Set.Pairwise.mono` `coe_subset` `subset_union_left` `subset_union_right` `exists_list_nodup_eq` `Multiset.coe_nodup` `List.Nodup.append` `List.disjoint_toFinset_iff_disjoint` `noncommProd_congr` `ext` `noncommProd_lemma` `Multiset.noncommProd.congr_simp` `Multiset.noncommProd_coe` `Semigroup.to_isLawfulIdentity` `Semigroup.to_isAssociative` `Multiset.map_congr` `List.dedup_eq_self`
`noncommSum_addCommute` 📖	mathematical	`Set.Pairwise` `SetLike.coe` `Finset` `instSetLike` `Function.onFun` `AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`noncommSum`	—	`Multiset.noncommSum_addCommute` `noncommSum_lemma` `Multiset.mem_map`
`noncommSum_add_distrib` 📖	mathematical	`Set.Pairwise` `SetLike.coe` `Finset` `instSetLike` `Function.onFun` `AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`noncommSum` `Pi.instAdd` `noncommSum_add_distrib_aux`	—	`cons_induction_on` `noncommSum_add_distrib_aux` `noncommSum_congr` `add_zero` `Set.Pairwise.mono` `mem_cons` `noncommSum_cons` `Pi.add_apply` `mem_cons_of_mem` `AddCommute.add_add_add_comm` `noncommSum_addCommute` `mem_cons_self`
`noncommSum_add_distrib_aux` 📖	mathematical	`Set.Pairwise` `SetLike.coe` `Finset` `instSetLike` `Function.onFun` `AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`Pi.instAdd`	—	`AddCommute.add_left` `AddCommute.add_right` `Set.Pairwise.of_refl` `AddCommute.on_refl` `AddCommute.symm`
`noncommSum_add_single` 📖	mathematical	—	`noncommSum` `Pi.addMonoid` `univ` `Pi.single` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Pi.single_apply_addCommute`	—	`noncommSum_single`
`noncommSum_congr` 📖	mathematical	`Set.Pairwise` `SetLike.coe` `Finset` `instSetLike` `Function.onFun` `AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`noncommSum`	—	`noncommSum_lemma` `Multiset.map_congr` `Multiset.noncommSum.congr_simp`
`noncommSum_cons` 📖	mathematical	`Finset` `instMembership` `Set.Pairwise` `SetLike.coe` `instSetLike` `cons` `Function.onFun` `AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`noncommSum` `Set.Pairwise.mono` `Multiset` `Multiset.instMembership` `val` `Set` `Set.instMembership` `mem_cons`	—	`Set.Pairwise.mono` `mem_cons` `noncommSum_lemma` `Multiset.map_cons` `Multiset.noncommSum.congr_simp` `Multiset.mem_cons_of_mem` `Multiset.noncommSum_cons`
`noncommSum_cons'` 📖	mathematical	`Finset` `instMembership` `Set.Pairwise` `SetLike.coe` `instSetLike` `cons` `Function.onFun` `AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`noncommSum` `Set.Pairwise.mono` `Multiset` `Multiset.instMembership` `val` `Set` `Set.instMembership` `mem_cons`	—	`Set.Pairwise.mono` `mem_cons` `noncommSum_lemma` `Multiset.map_cons` `Multiset.noncommSum.congr_simp` `Multiset.mem_cons_of_mem` `Multiset.noncommSum_cons'`
`noncommSum_empty` 📖	mathematical	`Set.Pairwise` `SetLike.coe` `Finset` `instSetLike` `instEmptyCollection` `Function.onFun` `AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`noncommSum` `AddZero.toZero`	—	—
`noncommSum_eq_card_nsmul` 📖	mathematical	`Set.Pairwise` `SetLike.coe` `Finset` `instSetLike` `Function.onFun` `AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`noncommSum` `AddMonoid.toNatSMul` `card`	—	`noncommSum_lemma` `noncommSum.eq_1` `Multiset.noncommSum_eq_card_nsmul` `Multiset.mem_map` `Multiset.card_map`
`noncommSum_eq_sum` 📖	mathematical	—	`noncommSum` `AddCommMonoid.toAddMonoid` `AddCommute.all` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `sum`	—	`cons_induction_on` `AddCommute.all` `Set.Pairwise.mono` `mem_cons` `noncommSum_cons` `sum_cons`
`noncommSum_induction` 📖	mathematical	`Set.Pairwise` `SetLike.coe` `Finset` `instSetLike` `Function.onFun` `AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddZero.toZero`	`noncommSum`	—	`Multiset.noncommSum_induction` `noncommSum_lemma` `Multiset.mem_map`
`noncommSum_insert_of_notMem` 📖	mathematical	`Set.Pairwise` `SetLike.coe` `Finset` `instSetLike` `instInsert` `Function.onFun` `AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instMembership`	`noncommSum` `Set.Pairwise.mono` `Multiset` `Multiset.instMembership` `val` `mem_insert_of_mem`	—	`Set.Pairwise.mono` `mem_insert_of_mem` `mem_cons` `cons_eq_insert` `noncommSum_congr` `noncommSum_cons`
`noncommSum_insert_of_notMem'` 📖	mathematical	`Set.Pairwise` `SetLike.coe` `Finset` `instSetLike` `instInsert` `Function.onFun` `AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instMembership`	`noncommSum` `Set.Pairwise.mono` `Multiset` `Multiset.instMembership` `val` `mem_insert_of_mem`	—	`Set.Pairwise.mono` `mem_insert_of_mem` `mem_cons` `cons_eq_insert` `noncommSum_congr` `noncommSum_cons'`
`noncommSum_lemma` 📖	mathematical	`Set.Pairwise` `SetLike.coe` `Finset` `instSetLike` `Function.onFun` `AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`setOf` `Multiset` `Multiset.instMembership` `Multiset.map` `val`	—	`Multiset.map_set_pairwise`
`noncommSum_single` 📖	mathematical	—	`noncommSum` `Pi.addMonoid` `univ` `Pi.single` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Pi.single_apply_addCommute`	—	`Pi.single_apply_addCommute` `AddCommute.map` `AddMonoidHomClass.toAddHomClass` `AddMonoidHom.instAddMonoidHomClass` `Set.Pairwise.of_refl` `AddCommute.on_refl` `map_noncommSum` `insert_erase` `mem_univ` `noncommSum_congr` `Set.Pairwise.mono` `mem_insert_of_mem` `noncommSum_insert_of_notMem` `notMem_erase` `noncommSum_eq_card_nsmul` `mem_erase` `nsmul_zero` `add_zero` `Pi.single_eq_same`
`noncommSum_singleton` 📖	mathematical	—	`noncommSum` `Finset` `instSingleton`	—	`add_zero`
`noncommSum_toFinset` 📖	mathematical	`Set.Pairwise` `SetLike.coe` `Finset` `instSetLike` `List.toFinset` `Function.onFun` `AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`noncommSum` `AddZero.toZero`	—	`noncommSum_lemma` `Multiset.map_congr` `List.dedup_eq_self` `Multiset.noncommSum.congr_simp` `Multiset.noncommSum_coe`
`noncommSum_union_of_disjoint` 📖	mathematical	`Disjoint` `Finset` `partialOrder` `instOrderBot` `Set.Pairwise` `setOf` `instMembership` `instUnion` `Function.onFun` `AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`noncommSum` `Set.Pairwise.mono` `SetLike.coe` `instSetLike` `Set` `Set.instHasSubset` `instHasSubset` `coe_subset` `subset_union_left` `subset_union_right`	—	`Set.Pairwise.mono` `coe_subset` `subset_union_left` `subset_union_right` `exists_list_nodup_eq` `Multiset.coe_nodup` `List.Nodup.append` `List.disjoint_toFinset_iff_disjoint` `mem_union` `List.mem_toFinset` `Set.ext_iff` `SetLike.mem_coe` `Multiset.mem_coe` `noncommSum_congr` `ext` `noncommSum_lemma` `Multiset.noncommSum.congr_simp` `Multiset.noncommSum_coe` `AddSemigroup.to_isLawfulIdentity` `AddSemigroup.to_isAssociative` `Multiset.map_congr` `List.dedup_eq_self`

MonoidHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`pi_ext` 📖	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Pi.mulOneClass` `Monoid.toMulOneClass` `instFunLike` `Pi.mulSingle` `MulOne.toOne`	—	—	`nonempty_fintype` `ext` `Pi.mulSingle_apply_commute` `Finset.noncommProd_mulSingle` `Commute.map` `MonoidHomClass.toMulHomClass` `instMonoidHomClass` `Set.Pairwise.of_refl` `Commute.on_refl` `Finset.map_noncommProd`

Multiset

Definitions

Name	Category	Theorems
`noncommFold` 📖	CompOp	4 math math: `noncommFold_eq_fold`, `noncommFold_coe`, `noncommFold_cons`, `noncommFold_empty`
`noncommFoldr` 📖	CompOp	4 math math: `noncommFoldr_eq_foldr`, `noncommFoldr_empty`, `noncommFoldr_cons`, `noncommFoldr_coe`
`noncommProd` 📖	CompOp	15 math math: `noncommProd_erase_mul`, `noncommProd_eq_prod`, `noncommProd_commute`, `Submonoid.multiset_noncommProd_mem`, `noncommProd_add`, `noncommProd_coe`, `map_noncommProd`, `noncommProd_induction`, `mul_noncommProd_erase`, `Finset.sum_pow_of_commute`, `noncommProd_eq_pow_card`, `noncommProd_cons'`, `noncommProd_cons`, `Subgroup.multiset_noncommProd_mem`, `noncommProd_empty`
`noncommSum` 📖	CompOp	12 math math: `noncommSum_cons'`, `noncommSum_eq_card_nsmul`, `AddSubgroup.multiset_noncommSum_mem`, `AddSubmonoid.multiset_noncommSum_mem`, `map_noncommSum`, `noncommSum_empty`, `noncommSum_add`, `noncommSum_addCommute`, `noncommSum_cons`, `noncommSum_induction`, `noncommSum_coe`, `noncommSum_eq_sum`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_noncommProd` 📖	mathematical	`Set.Pairwise` `setOf` `Multiset` `instMembership` `Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`DFunLike.coe` `noncommProd` `map` `map_noncommProd_aux` `MonoidHomClass.toMulHomClass`	—	`map_noncommProd_aux` `MonoidHomClass.toMulHomClass` `noncommProd_coe` `map_list_prod`
`map_noncommProd_aux` 📖	mathematical	`Set.Pairwise` `setOf` `Multiset` `instMembership` `Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`map` `DFunLike.coe`	—	`Commute.map` `Set.Pairwise.of_refl` `Commute.instRefl`
`map_noncommSum` 📖	mathematical	`Set.Pairwise` `setOf` `Multiset` `instMembership` `AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`DFunLike.coe` `noncommSum` `map` `map_noncommSum_aux` `AddMonoidHomClass.toAddHomClass`	—	`map_noncommSum_aux` `AddMonoidHomClass.toAddHomClass` `noncommSum_coe` `map_list_sum`
`map_noncommSum_aux` 📖	mathematical	`Set.Pairwise` `setOf` `Multiset` `instMembership` `AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`map` `DFunLike.coe`	—	`mem_map` `AddCommute.map` `Set.Pairwise.of_refl` `AddCommute.instRefl`
`mul_noncommProd_erase` 📖	mathematical	`Multiset` `instMembership` `Set.Pairwise` `setOf` `Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `mem_of_mem_erase`	`noncommProd` `erase`	—	`noncommProd_coe` `eq_or_ne` `List.prod_erase_of_comm`
`noncommFold_coe` 📖	mathematical	`Set.Pairwise` `setOf` `Multiset` `instMembership` `ofList`	`noncommFold`	—	`noncommFoldr_coe`
`noncommFold_cons` 📖	mathematical	`Set.Pairwise` `setOf` `Multiset` `instMembership` `cons`	`noncommFold`	—	`noncommFold_coe`
`noncommFold_empty` 📖	mathematical	`Set.Pairwise` `setOf` `Multiset` `instMembership` `instZero`	`noncommFold`	—	—
`noncommFold_eq_fold` 📖	mathematical	—	`noncommFold` `fold`	—	`noncommFold_coe`
`noncommFoldr_coe` 📖	mathematical	`Set.Pairwise` `setOf` `Multiset` `instMembership` `ofList`	`noncommFoldr`	—	—
`noncommFoldr_cons` 📖	mathematical	`Set.Pairwise` `setOf` `Multiset` `instMembership` `cons`	`noncommFoldr`	—	`noncommFoldr_coe`
`noncommFoldr_empty` 📖	mathematical	`Set.Pairwise` `setOf` `Multiset` `instMembership` `instZero`	`noncommFoldr`	—	—
`noncommFoldr_eq_foldr` 📖	mathematical	—	`noncommFoldr` `LeftCommutative.left_comm` `foldr`	—	`LeftCommutative.left_comm` `noncommFoldr_coe`
`noncommProd_add` 📖	mathematical	`Set.Pairwise` `setOf` `Multiset` `instMembership` `instAdd` `Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`noncommProd` `Set.Pairwise.mono` `subset_of_le` `le_add_right` `le_add_left`	—	`Set.Pairwise.mono` `subset_of_le` `le_add_right` `le_add_left` `noncommProd_coe` `Semigroup.to_isLawfulIdentity` `Semigroup.to_isAssociative`
`noncommProd_coe` 📖	mathematical	`Set.Pairwise` `setOf` `Multiset` `instMembership` `ofList` `Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`noncommProd` `MulOne.toOne`	—	`noncommProd.eq_1` `noncommFold_coe`
`noncommProd_commute` 📖	mathematical	`Set.Pairwise` `setOf` `Multiset` `instMembership` `Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`noncommProd`	—	`noncommProd_coe` `Commute.list_prod_right`
`noncommProd_cons` 📖	mathematical	`Set.Pairwise` `setOf` `Multiset` `instMembership` `cons` `Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`noncommProd` `Set.Pairwise.mono` `mem_cons_of_mem`	—	`Set.Pairwise.mono` `mem_cons_of_mem` `noncommProd_coe`
`noncommProd_cons'` 📖	mathematical	`Set.Pairwise` `setOf` `Multiset` `instMembership` `cons` `Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`noncommProd` `Set.Pairwise.mono` `mem_cons_of_mem`	—	`Set.Pairwise.mono` `mem_cons_of_mem` `noncommProd_coe` `mul_one` `one_mul` `mul_assoc` `Set.Pairwise.of_refl` `Commute.instRefl`
`noncommProd_empty` 📖	mathematical	`Set.Pairwise` `setOf` `Multiset` `instMembership` `instZero` `Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`noncommProd` `MulOne.toOne`	—	—
`noncommProd_eq_pow_card` 📖	mathematical	`Set.Pairwise` `setOf` `Multiset` `instMembership` `Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`noncommProd` `Monoid.toNatPow` `card`	—	`noncommProd_coe` `List.prod_eq_pow_card`
`noncommProd_eq_prod` 📖	mathematical	—	`noncommProd` `CommMonoid.toMonoid` `Commute.all` `CommSemigroup.toCommMagma` `CommMonoid.toCommSemigroup` `prod`	—	`Commute.all` `noncommProd_coe`
`noncommProd_erase_mul` 📖	mathematical	`Multiset` `instMembership` `Set.Pairwise` `setOf` `Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `mem_of_mem_erase`	`noncommProd` `erase`	—	`eq_or_ne` `mem_of_mem_erase` `Commute.eq` `noncommProd_commute` `mul_noncommProd_erase`
`noncommProd_induction` 📖	mathematical	`Set.Pairwise` `setOf` `Multiset` `instMembership` `Commute` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne`	`noncommProd`	—	`noncommProd_coe` `List.prod_induction`
`noncommSum_add` 📖	mathematical	`Set.Pairwise` `setOf` `Multiset` `instMembership` `instAdd` `AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`noncommSum` `Set.Pairwise.mono` `subset_of_le` `le_add_right` `le_add_left`	—	`Set.Pairwise.mono` `subset_of_le` `le_add_right` `le_add_left` `noncommSum_coe` `AddSemigroup.to_isLawfulIdentity` `AddSemigroup.to_isAssociative`
`noncommSum_addCommute` 📖	mathematical	`Set.Pairwise` `setOf` `Multiset` `instMembership` `AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`noncommSum`	—	`noncommSum_coe` `AddCommute.list_sum_right`
`noncommSum_coe` 📖	mathematical	`Set.Pairwise` `setOf` `Multiset` `instMembership` `ofList` `AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`noncommSum` `AddZero.toZero`	—	`noncommSum.eq_1` `noncommFold_coe`
`noncommSum_cons` 📖	mathematical	`Set.Pairwise` `setOf` `Multiset` `instMembership` `cons` `AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`noncommSum` `Set.Pairwise.mono` `mem_cons_of_mem`	—	`Set.Pairwise.mono` `mem_cons_of_mem` `noncommSum_coe`
`noncommSum_cons'` 📖	mathematical	`Set.Pairwise` `setOf` `Multiset` `instMembership` `cons` `AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`noncommSum` `Set.Pairwise.mono` `mem_cons_of_mem`	—	`Set.Pairwise.mono` `mem_cons_of_mem` `noncommSum_coe` `add_zero` `zero_add` `add_assoc` `mem_coe` `Set.Pairwise.of_refl` `AddCommute.instRefl`
`noncommSum_empty` 📖	mathematical	`Set.Pairwise` `setOf` `Multiset` `instMembership` `instZero` `AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`noncommSum` `AddZero.toZero`	—	—
`noncommSum_eq_card_nsmul` 📖	mathematical	`Set.Pairwise` `setOf` `Multiset` `instMembership` `AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`noncommSum` `AddMonoid.toNatSMul` `card`	—	`noncommSum_coe` `List.sum_eq_card_nsmul` `mem_coe`
`noncommSum_eq_sum` 📖	mathematical	—	`noncommSum` `AddCommMonoid.toAddMonoid` `AddCommute.all` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `sum`	—	`AddCommute.all` `noncommSum_coe`
`noncommSum_induction` 📖	mathematical	`Set.Pairwise` `setOf` `Multiset` `instMembership` `AddCommute` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddZero.toZero`	`noncommSum`	—	`noncommSum_coe` `List.sum_induction` `mem_coe`

---

← Back to Index