Commit 2023-01-19 17:27 dd4871d2

View on Github →

feat: port Data.Finset.NoncommProd (#1681)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Finset/NoncommProd.lean

added def Finset.noncommProd

added theorem Finset.noncommProd_commute

added theorem Finset.noncommProd_congr

added theorem Finset.noncommProd_empty

added theorem Finset.noncommProd_eq_pow_card

added theorem Finset.noncommProd_eq_prod

added theorem Finset.noncommProd_insert_of_not_mem'

added theorem Finset.noncommProd_insert_of_not_mem

added theorem Finset.noncommProd_lemma

added theorem Finset.noncommProd_map

added theorem Finset.noncommProd_mul_distrib

added theorem Finset.noncommProd_mul_distrib_aux

added theorem Finset.noncommProd_mul_single

added theorem Finset.noncommProd_singleton

added theorem Finset.noncommProd_toFinset

added theorem Finset.noncommProd_union_of_disjoint

added theorem MonoidHom.pi_ext

added def Multiset.noncommFold

added theorem Multiset.noncommFold_coe

added theorem Multiset.noncommFold_cons

added theorem Multiset.noncommFold_empty

added theorem Multiset.noncommFold_eq_fold

added def Multiset.noncommFoldr

added theorem Multiset.noncommFoldr_coe

added theorem Multiset.noncommFoldr_cons

added theorem Multiset.noncommFoldr_empty

added theorem Multiset.noncommFoldr_eq_foldr

added def Multiset.noncommProd

added theorem Multiset.noncommProd_add

added theorem Multiset.noncommProd_coe

added theorem Multiset.noncommProd_commute

added theorem Multiset.noncommProd_cons'

added theorem Multiset.noncommProd_cons

added theorem Multiset.noncommProd_empty

added theorem Multiset.noncommProd_eq_pow_card

added theorem Multiset.noncommProd_eq_prod

added theorem Multiset.noncommProd_map