Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2022-03-12 04:22
1eaf4999
View on Github →
feat(group_theory/subgroup/basic): {multiset_,}noncomm_prod_mem (
#12523
) and same for submonoids.
Estimated changes
Modified
src/group_theory/subgroup/basic.lean
added
theorem
subgroup.multiset_noncomm_prod_mem
added
theorem
subgroup.noncomm_prod_mem
Modified
src/group_theory/submonoid/membership.lean
added
theorem
submonoid.multiset_noncomm_prod_mem
added
theorem
submonoid.noncomm_prod_mem