Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-14 23:58 31263840

View on Github →

refactor(data/finset/noncomm_prod): Use set.pairwise (#16859) Redefine the various noncomm_prods using set.pairwise. This has the advantage of having a solid API around monotonicity in the set or in the relation and avoiding checking the trivial i = j case.

Estimated changes

added theorem list.coe_to_finset
modified def finset.noncomm_prod
modified theorem finset.noncomm_prod_commute
modified theorem finset.noncomm_prod_congr
modified theorem finset.noncomm_prod_empty
modified theorem finset.noncomm_prod_map
modified theorem monoid_hom.pi_ext
modified def multiset.noncomm_fold
modified theorem multiset.noncomm_fold_coe
modified theorem multiset.noncomm_fold_cons
modified theorem multiset.noncomm_fold_empty
modified theorem multiset.noncomm_foldr_coe
modified theorem multiset.noncomm_foldr_cons
modified def multiset.noncomm_prod
modified theorem multiset.noncomm_prod_coe
modified theorem multiset.noncomm_prod_cons'
modified theorem multiset.noncomm_prod_cons
modified theorem multiset.noncomm_prod_empty
modified theorem multiset.noncomm_prod_map
modified theorem subgroup.noncomm_prod_mem
modified theorem submonoid.noncomm_prod_mem