mathlib

543fcef1 - chore(algebra/group_power/lemmas): minimize imports (#10246)

chore(algebra/group_power/lemmas): minimize imports (#10246) Most of these were imported transitively anyway, but `data.list.basic` is unneeded. Co-authored-by: Johan Commelin <johan@commelin.net>