Commit 2021-10-25 17:43 0d131fe5

chore(group_theory/submonoid): move a lemma to reduce imports (#9951) Currently, algebra.pointwise is a relatively "heavy" import (e.g., it depends on data.set.finite) and I want to use submonoid closures a bit earlier than that.