adomani: test a trivial addition

adomani commented 3 months ago

maintainer merge

github-actions[bot] commented 3 months ago

PR summary c5a51bf7f

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

```bash ## summary with just the declaration names: ./scripts/declarations_diff.sh ## more verbose report: ./scripts/declarations_diff.sh long ```

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

adomani commented 3 months ago

maintainer merge

adomani commented 3 months ago

maintainer merge

adomani commented 3 months ago

maintainer merge

adomani commented 3 months ago

maintainer merge

adomani commented 3 months ago

maintainer merge

adomani commented 3 months ago

maintainer merge

adomani commented 3 months ago

maintainer merge

adomani commented 3 months ago

maintainer merge

adomani commented 3 months ago

maintainer merge

adomani commented 3 months ago

maintainer merge

bryangingechen commented 3 months ago

maintainer merge

bryangingechen commented 3 months ago

maintainer merge

adomani commented 3 months ago

maintainer merge

github-actions[bot] commented 3 months ago

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

adomani commented 3 months ago

maintainer merge

github-actions[bot] commented 3 months ago

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

adomani commented 3 months ago

maintainer merge

github-actions[bot] commented 3 months ago

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

adomani commented 3 months ago

maintainer merge

github-actions[bot] commented 3 months ago

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

adomani commented 3 months ago

maintainer merge

github-actions[bot] commented 3 months ago

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

adomani commented 3 months ago

maintainer merge

github-actions[bot] commented 3 months ago

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

adomani commented 3 months ago

maintainer merge

github-actions[bot] commented 3 months ago

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

adomani commented 3 months ago

maintainer merge

github-actions[bot] commented 3 months ago

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

adomani commented 3 months ago

maintainer merge

github-actions[bot] commented 3 months ago

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

adomani commented 2 months ago

The corresponding mathlib PR implementing maintainer merges split by topics has been merged, fixed and tested!

bryangingechen / mathlib4