Commit 2024-12-02 07:36 720f1785

View on Github →

chore: split Algebra.Submonoid.Membership (#19628) This file had two unrelated parts, one about big operators and one about other facts about membership.

Estimated changes

added theorem Submonoid.prod_mem
added theorem list_prod_mem
added theorem multiset_prod_mem
added theorem prod_mem
deleted theorem Submonoid.coe_finset_prod
deleted theorem Submonoid.coe_list_prod
deleted theorem Submonoid.list_prod_mem
deleted theorem Submonoid.noncommProd_mem
deleted theorem Submonoid.prod_mem
deleted theorem list_prod_mem
deleted theorem multiset_prod_mem
deleted theorem prod_mem