[Merged by Bors] - chore: drop some unnecessary imports

[hrmacbeth]

---

[semorrison]

I think the actual problem here is that Riccardo put the wrong imports in Mathlib.Algebra.Order.Hom.Basic when porting!

[semorrison]

i.e. the correct fix is to revert your change, and replace the import block in Mathlib.Algebra.Order.Hom.Basic with

import Mathlib.Algebra.GroupPower.Order

(I identified this by trying to backport.)

[semorrison]

Please merge if CI accepts leanprover-community/mathlib#18978!

bors d+

[bors]

✌️ hrmacbeth can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[eric-wieser]

Just a reminder that we should not update the SHA for this file in this PR, as there are other changes which would need forward-porting first.

[jcommelin]

Thanks 🎉

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style