Commit 2022-04-21 20:30 efab188a
View on Github →refactor(group_theory/{submonoid, subsemigroup}/basic): move mul_mem_class
(#13559)
This moves mul_mem_class
(and add_mem_class
) from group_theory/submonoid/basic
to group_theory/subsemigroup/basic
so that subsemigroup
can be an instance. We then protect subsemigroup.mul_mem
. In addition, we add an induction principle for binary predicates to better parallel group_theory/submonoid/basic
.