feat: add ContinuousSMul instances for ℚ≥0
#239664
Triggered via pull request
October 19, 2025 09:04
astrainfinita
astrainfinita
synchronize
#28474
Status
Failure
Total duration
24m 50s
Artifacts
1
build_fork.yml
on: pull_request_target
Build (fork)
24m 48s
Lint style (fork)
3m 13s
Post-CI job (fork)
0s
Annotations
2 errors
|
Build (fork)
Process completed with exit code 1.
|
|
Build (fork):
Mathlib/Topology/Instances/Rat.lean#L131
@NNRat.instContinuousSMulOfRingOfRat argument 2 inst✝³ : Ring
|
Artifacts
Produced during runtime
| Name | Size | Digest | |
|---|---|---|---|
|
mathlib4_artifact
|
1.65 GB |
sha256:a3c4a76ff663539f02cec0fb6addf9e190d8a63adc921334652d0aef12da30c4
|
|