mathlib-bors[bot]

:v: xroblot can now approve this pull request. To approve and merge a pull request, simply reply with `bors r+`. More detailed instructions are available [here](https://bors.tech/documentation/getting-started/#reviewing-pull-requests).

Pull request successfully merged into master. Build succeeded: * [Build](https://github.com/leanprover-community/mathlib4/actions/runs/10998808806/job/30537565301) * [Lint style](https://github.com/leanprover-community/mathlib4/actions/runs/10998808806/job/30537564672)

Pull request successfully merged into master. Build succeeded: * [Build](https://github.com/leanprover-community/mathlib4/actions/runs/9191451749/job/25277881763) * [Check all files imported](https://github.com/leanprover-community/mathlib4/actions/runs/9191451749/job/25277881459) * [Lint style](https://github.com/leanprover-community/mathlib4/actions/runs/9191451749/job/25277881032)

Pull request successfully merged into master. Build succeeded: * [Build](https://github.com/leanprover-community/mathlib4/actions/runs/9227496919/job/25389562400) * [Check all files imported](https://github.com/leanprover-community/mathlib4/actions/runs/9227496919/job/25389561785) * [Lint style](https://github.com/leanprover-community/mathlib4/actions/runs/9227496919/job/25389562611)

Pull request successfully merged into master. Build succeeded: * [Build](https://github.com/leanprover-community/mathlib4/actions/runs/9190991794/job/25276450999) * [Check all files imported](https://github.com/leanprover-community/mathlib4/actions/runs/9190991794/job/25276450405) * [Lint style](https://github.com/leanprover-community/mathlib4/actions/runs/9190991794/job/25276449597)

Pull request successfully merged into master. Build succeeded: * [Build](https://github.com/leanprover-community/mathlib4/actions/runs/9192331709/job/25280702548) * [Check all files imported](https://github.com/leanprover-community/mathlib4/actions/runs/9192331709/job/25280702239) * [Lint style](https://github.com/leanprover-community/mathlib4/actions/runs/9192331709/job/25280701807)

Pull request successfully merged into master. Build succeeded: * [Build](https://github.com/leanprover-community/mathlib4/actions/runs/9328045334/job/25678715111) * [Check all files imported](https://github.com/leanprover-community/mathlib4/actions/runs/9328045334/job/25678715163) * [Lint style](https://github.com/leanprover-community/mathlib4/actions/runs/9328045334/job/25678715277)

Pull request successfully merged into master. Build succeeded: * [Build](https://github.com/leanprover-community/mathlib4/actions/runs/9687435100/job/26732055698) * [Lint style](https://github.com/leanprover-community/mathlib4/actions/runs/9687435100/job/26732055483)

Build failed: * [Build](https://github.com/leanprover-community/mathlib4/actions/runs/9112323989/job/25051350483)

:v: grunweg can now approve this pull request. To approve and merge a pull request, simply reply with `bors r+`. More detailed instructions are available [here](https://bors.tech/documentation/getting-started/#reviewing-pull-requests).