Skip to content

[Merged by Bors] - feat(RingTheory/IsTensorProduct): heterogeneous associativity #271480

[Merged by Bors] - feat(RingTheory/IsTensorProduct): heterogeneous associativity

[Merged by Bors] - feat(RingTheory/IsTensorProduct): heterogeneous associativity #271480

Triggered via pull request February 20, 2026 23:44
@chrisflavchrisflav
synchronize #35557
Status Success
Total duration 23m 18s
Artifacts 2

build_fork.yml

on: pull_request_target
ci (fork)  /  Upload to cache
56s
ci (fork) / Upload to cache
ci (fork)  /  Post-Build Step
2m 41s
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
63.8 MB
sha256:8c5c6402ea772d67fa61db59f8c0d8e0a37ba49415f925454552dec95b72dfcd
import-graph Expired
276 KB
sha256:02992f832d417c9bda9e8a0e7e7d67e258910fb8cbf1fb5f5d43058072f2ed73