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.