[Merged by Bors] - chore: add dependabot

[pitmonticone]

This PR introduces a Dependabot configuration specifically for managing dependencies in GitHub Actions workflows.

It automates the process of checking for updates to GitHub Actions dependencies.

---

[github-actions]

PR summary 956eea66a5

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

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

You can run this locally as follows

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

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

The doc-module for script/declarations_diff.sh contains some details about this script.

[grunweg]

IIRC, other repositories like the queueboard have "monthly" here. Do you have a particular reason for the different frequency?

[pitmonticone]

Nope, I can change that immediately.

[pitmonticone]

Done @grunweg. Thanks.

[grunweg]

This is my first time reviewing such a file --- cross-checking github's documentation about this, this looks sensible. Thanks for automating this!

Can you add some brief explanation what this does to the PR description? Thanks! Never mind, you already did that.
maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by grunweg.

[bryangingechen]

Thanks!
bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Lint style
• Build

[bryangingechen]

Ah, it's not the end of the world, but since depandabot isn't aware of our bors.in.yml system, we won't be able to use its PRs as is for those updates. cf. #18017 .

I'll go through and do a manual update including all the updates now.

The manual update PR is at #18026

[grunweg]

(These PRs also broke the queueboard, as the PR author doesn't have a standard github handle --- but this was easy to fix. I was also surprised by this.)