group is a very heavy tactic (it imports ring to normalise exponents) which is no more powerful than simp [mul_assoc] in many cases appearing in practice. It might be useful to have a lightweight variant of group (in the sense that it doesn't import Field or even MonoidWithZero) for those numerous cases.

Zulip

List of PRs removing uses of group:

• [Merged by Bors] - chore(GroupTheory/Commutator): don't import Ring #21296