[Merged by Bors] - chore: remove unused Category assumption
#6972
Triggered via issue
November 23, 2024 19:24
mathlib-bors[bot]
Status
Success
Total duration
10s
Artifacts
–
maintainer_merge.yml
on: issue_comment
Ping maintainers on Zulip
2s