[Merged by Bors] - feat: SeparatelyContinuousMul class for multiplication which is continuous in each variable
#271468
j-loreauxbuild_fork.yml
on: pull_request_target
ci (fork)
/
Build
5m 20s
ci (fork)
/
Lint style
1m 59s
ci (fork)
/
Post-CI job
0s
Annotations
20 errors and 21 warnings
|
ci (fork) / Build
@[to_additive] failed to add declaration `Homeomorph.addRight._proof_1`.
|
|
ci (fork) / Build
`simp` made no progress
|
|
ci (fork) / Build
@[to_additive] failed to add declaration `Filter.map_add_left_nhdsNE`.
|
|
ci (fork) / Build
@[to_additive] failed to add declaration `IsClosed.left_addCoset`.
|
|
ci (fork) / Build
@[to_additive] failed to add declaration `isClosedMap_add_left`.
|
|
ci (fork) / Build
@[to_additive] failed to add declaration `IsOpen.left_addCoset`.
|
|
ci (fork) / Build
@[to_additive] failed to add declaration `isOpenMap_add_left`.
|
|
ci (fork) / Build
@[to_additive] failed to add declaration `Homeomorph.addLeft_symm`.
|
|
ci (fork) / Build
@[to_additive] failed to add declaration `Homeomorph.coe_addLeft`.
|
|
ci (fork) / Build
@[to_additive] failed to add declaration `Homeomorph.addLeft._proof_1`.
|
|
ci (fork) / Build
@[to_additive] failed to add declaration `Homeomorph.addRight._proof_1`.
|
|
ci (fork) / Build
`simp` made no progress
|
|
ci (fork) / Build
@[to_additive] failed to add declaration `Filter.map_add_left_nhdsNE`.
|
|
ci (fork) / Build
@[to_additive] failed to add declaration `IsClosed.left_addCoset`.
|
|
ci (fork) / Build
@[to_additive] failed to add declaration `isClosedMap_add_left`.
|
|
ci (fork) / Build
@[to_additive] failed to add declaration `IsOpen.left_addCoset`.
|
|
ci (fork) / Build
@[to_additive] failed to add declaration `isOpenMap_add_left`.
|
|
ci (fork) / Build
@[to_additive] failed to add declaration `Homeomorph.addLeft_symm`.
|
|
ci (fork) / Build
@[to_additive] failed to add declaration `Homeomorph.coe_addLeft`.
|
|
ci (fork) / Build
@[to_additive] failed to add declaration `Homeomorph.addLeft._proof_1`.
|
|
ci (fork) / Build
`continuous_mul_left` has been deprecated: Use `continuous_const_mul` instead
|
|
ci (fork) / Build
`continuous_mul_right` has been deprecated: Use `continuous_mul_const` instead
|
|
ci (fork) / Build
declaration uses `sorry`
|
|
ci (fork) / Build
declaration uses `sorry`
|
|
ci (fork) / Build
declaration uses `sorry`
|
|
ci (fork) / Build
declaration uses `sorry`
|
|
ci (fork) / Build
`continuous_mul_right` has been deprecated: Use `continuous_mul_const` instead
|
|
ci (fork) / Build
`continuous_mul_right` has been deprecated: Use `continuous_mul_const` instead
|
|
ci (fork) / Build
`continuous_mul_left` has been deprecated: Use `continuous_const_mul` instead
|
|
ci (fork) / Build
`continuous_mul_left` has been deprecated: Use `continuous_const_mul` instead
|
|
ci (fork) / Build
`continuous_mul_left` has been deprecated: Use `continuous_const_mul` instead
|
|
ci (fork) / Build
`continuous_mul_right` has been deprecated: Use `continuous_mul_const` instead
|
|
ci (fork) / Build
declaration uses `sorry`
|
|
ci (fork) / Build
declaration uses `sorry`
|
|
ci (fork) / Build
declaration uses `sorry`
|
|
ci (fork) / Build
declaration uses `sorry`
|
|
ci (fork) / Build
`continuous_mul_right` has been deprecated: Use `continuous_mul_const` instead
|
|
ci (fork) / Build
`continuous_mul_right` has been deprecated: Use `continuous_mul_const` instead
|
|
ci (fork) / Build
`continuous_mul_left` has been deprecated: Use `continuous_const_mul` instead
|
|
ci (fork) / Build
`continuous_mul_left` has been deprecated: Use `continuous_const_mul` instead
|
|
ci (fork) / Build
Cache directory does not exist: /home/lean/.cache/mathlib
|
Artifacts
Produced during runtime
| Name | Size | Digest | |
|---|---|---|---|
|
cache-staging
|
18.5 MB |
sha256:9273dc1e0c70674a32bdb10456d3d3c4b6aa009857f542b599ac7de6f8cf5dff
|
|