Skip to content

[Merged by Bors] - style(CategoryTheory/Monoidal): add notation for whiskerLeftIso and whiskerRightIso #271481

[Merged by Bors] - style(CategoryTheory/Monoidal): add notation for whiskerLeftIso and whiskerRightIso

[Merged by Bors] - style(CategoryTheory/Monoidal): add notation for whiskerLeftIso and whiskerRightIso #271481

Triggered via pull request February 20, 2026 23:51
@parabamoghvparabamoghv
synchronize #35010
Status Success
Total duration 22m 44s
Artifacts 2

build_fork.yml

on: pull_request_target
ci (fork)  /  Upload to cache
45s
ci (fork) / Upload to cache
ci (fork)  /  Post-Build Step
2m 43s
ci (fork) / Post-Build Step
ci (fork)  /  Post-CI job
5s
ci (fork) / Post-CI job
Fit to window
Zoom out
Zoom in

Annotations

1 warning
ci (fork) / Build
Cache directory does not exist: /home/lean/.cache/mathlib

Artifacts

Produced during runtime
Name Size Digest
cache-staging
67.5 MB
sha256:7788d6cbc15d43fbf712f137e9de2bac5040e9ccf77cf5d63bdd857164511dce
import-graph Expired
275 KB
sha256:e19e99013d1a1f8e5e22dd178f2c23e100bb1d15104e7bc2067dc003d541e912