[Merged by Bors] - feat: equivalent characterisation of split continuous linear maps #271463
grunwegbuild_fork.yml
on: pull_request_target
ci (fork)
/
Build
8m 53s
ci (fork)
/
Lint style
2m 0s
ci (fork)
/
Post-CI job
10s
Annotations
1 warning
|
ci (fork) / Build
Cache directory does not exist: /home/lean/.cache/mathlib
|
Artifacts
Produced during runtime
| Name | Size | Digest | |
|---|---|---|---|
|
cache-staging
|
2.02 MB |
sha256:aa3a9c34d087de1172c6937dd7ff61018bba24aaed5e0f1f9b7112d2f753c570
|
|
|
import-graph
Expired
|
273 KB |
sha256:44e30556840cf426a79082249dd2977679cedccfc2c8a4ff4a1e721216db0d97
|
|