chore(Charpoly/Disc): use nontriviality to drop a Nontrivial assu…
#21542
mathlib-bors[bot]bors.yml
on: push
ci (staging)
/
Build
14m 45s
ci (staging)
/
Lint style
2m 3s
ci (staging)
/
Post-CI job
10s
Annotations
1 warning
|
ci (staging) / Build
Cache directory does not exist: /home/lean/.cache/mathlib
|
Artifacts
Produced during runtime
| Name | Size | Digest | |
|---|---|---|---|
|
import-graph
|
273 KB |
sha256:6eebca1bfc74d2dc5c37403044af59a16cb9ac76aba5f6b93c858923ace6de5b
|
|