chore: move unitsEquivNeZero later #145281
Ruben-VandeVeldebuild.yml
on: push
Cancel Previous Runs (CI)
2s
Post-CI job
0s
Annotations
1 error and 2 warnings
|
Build
The process '/usr/bin/env' failed with exit code 1
|
|
Build:
Mathlib/Algebra/GroupWithZero/Units/Basic.lean#L8
unused import (use `lake exe shake --fix` to fix this, or `lake exe shake --update` to ignore)
|
|
Build:
Mathlib/Algebra/GroupWithZero/Units/Basic.lean#L13
unused import (use `lake exe shake --fix` to fix this, or `lake exe shake --update` to ignore)
|
Artifacts
Produced during runtime
| Name | Size | |
|---|---|---|
|
import-graph
|
178 KB |
|