chore: split order synonym instances for GroupWithZero into their own file

[Ruben-VandeVelde]

trafficstars

This is consistent with the Group file, and drops the dependency on Mathlib.Order entirely.

---

• [x] depends on: #13008
• [x] depends on: #13033

[Ruben-VandeVelde]

Will do.

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#13008~~
• ~~leanprover-community/mathlib4#13033~~ By Dependent Issues (🤖). Happy coding!

[github-actions[bot]]

No declarations were harmed in the making of this PR! 🐙

---

You can run this locally as follows

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

[Ruben-VandeVelde]

maintainer merge

(from Yaël earlier; just needed to merge master)

[github-actions[bot]]

🚀 Pull request has been placed on the maintainer queue by Ruben-VandeVelde.

[kbuzzard]

Thanks a lot for this busywork!

bors merge

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style