Mathlib v3 is deprecated. Go to Mathlib v4

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.

Estimated changes