Skip to content

[Merged by Bors] - feat(CategoryTheory/ChosenFiniteProducts): Add Mono instances for lifts of mono for ChosenFiniteProducts #58920

[Merged by Bors] - feat(CategoryTheory/ChosenFiniteProducts): Add Mono instances for lifts of mono for ChosenFiniteProducts

[Merged by Bors] - feat(CategoryTheory/ChosenFiniteProducts): Add Mono instances for lifts of mono for ChosenFiniteProducts #58920

Triggered via issue October 9, 2024 14:36
Status Success
Total duration 12s
Artifacts

add_label_from_comment.yml

on: issue_comment
Add ready-to-merge label
4s
Add ready-to-merge label
Add delegated label
0s
Add delegated label
Fit to window
Zoom out
Zoom in

Annotations

1 warning
Add ready-to-merge label
Unexpected input(s) 'repository', 'issue_number', 'labels', valid inputs are ['route', 'mediaType']