Skip to content

[Merged by Bors] - chore(Algebra/BigOperators/Finsupp/Basic): golf liftAddHom #271458

[Merged by Bors] - chore(Algebra/BigOperators/Finsupp/Basic): golf liftAddHom

[Merged by Bors] - chore(Algebra/BigOperators/Finsupp/Basic): golf liftAddHom #271458

Triggered via pull request February 20, 2026 20:35
@SnirBroshiSnirBroshi
synchronize #35570
Status Success
Total duration 36m 16s
Artifacts 2

build_fork.yml

on: pull_request_target
ci (fork)  /  Upload to cache
43s
ci (fork) / Upload to cache
ci (fork)  /  Post-Build Step
2m 38s
ci (fork) / Post-Build Step
ci (fork)  /  Post-CI job
6s
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
148 MB
sha256:2a42699597fd39fcb3cda53594baf75067dc8e41bbd6de4ff27ad9877733d264
import-graph Expired
275 KB
sha256:d4006fe44e6bb2fc84ae20a824c0a93d76e7867cbf611e68b3f34c1a16de0c1a