[Merged by Bors] - chore(Algebra/Order/Module/PositiveLinearMap): generalize OrderHomClass.ofLinear
#232656
Triggered via pull request
September 15, 2025 14:01
themathqueen
synchronize
#29626
Status
Success
Total duration
15m 37s
Artifacts
2
build_fork.yml
on: pull_request_target
Lint style (fork)
2m 8s
Build (fork)
11m 20s
Post-CI job (fork)
6s
CI Success
3s
Artifacts
Produced during runtime
Name | Size | Digest | |
---|---|---|---|
import-graph
Expired
|
241 KB |
sha256:a45b42d5fcedeebf7276a93c4fdb5937f3f07c36fa9213a656bdc217f9afdcb5
|
|
mathlib4_artifact
|
1.56 GB |
sha256:da9eb7ef270f7e9d5a632b240e323e8b3a554c68d470de373b65bb436c7632db
|
|