mathlib

0d131fe5 - chore(group_theory/submonoid): move a lemma to reduce imports (#9951)

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.