Skip to content

[Merged by Bors] - chore(Algebra/Order/Module/PositiveLinearMap): generalize OrderHomClass.ofLinear #232656

[Merged by Bors] - chore(Algebra/Order/Module/PositiveLinearMap): generalize OrderHomClass.ofLinear

[Merged by Bors] - chore(Algebra/Order/Module/PositiveLinearMap): generalize OrderHomClass.ofLinear #232656

Triggered via pull request September 15, 2025 14:01
@themathqueenthemathqueen
synchronize #29626
Status Success
Total duration 15m 37s
Artifacts 2

build_fork.yml

on: pull_request_target
Post-Build Step (fork)
2m 9s
Post-Build Step (fork)
Post-CI job (fork)
6s
Post-CI job (fork)
CI Success
3s
CI Success
Fit to window
Zoom out
Zoom in

Artifacts

Produced during runtime
Name Size Digest
import-graph Expired
241 KB
sha256:a45b42d5fcedeebf7276a93c4fdb5937f3f07c36fa9213a656bdc217f9afdcb5
mathlib4_artifact
1.56 GB
sha256:da9eb7ef270f7e9d5a632b240e323e8b3a554c68d470de373b65bb436c7632db