mathlib
f749197b - chore(algebra/group_power/basic): reduce imports (#17334)

Commit
3 years ago
chore(algebra/group_power/basic): reduce imports (#17334) * [after.pdf](https://leanprover.zulipchat.com/user_uploads/3121/R1Gg-EUylJs9H_GH1ERnKAX4/after.pdf) * [before.pdf](https://leanprover.zulipchat.com/user_uploads/user_uploads/3121/xYgoBBhTlgAaD_boJtN6ZHHO/before.pdf) Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Author
Parents
Loading