mathlib3

ec118ddc - ci(.github/workflows/*): lint PR style on GitHub runners (#9198)

ci(.github/workflows/*): lint PR style on GitHub runners (#9198) Since the style linter usually finishes in just a few seconds, we can move it off our self-hosted runners to give PR authors quicker feedback when the build queue is long. We do this only for PR runs, so that `bors` won't be held up in case the GitHub runners are backed up for whatever reason.