feat: a nonarchimedean group is totally disconnected (#16687) #11113
mathlib-bors[bot]bors.yml
on: push
Cancel Previous Runs (CI)
4s
Post-CI job
0s
Annotations
1 error and 2 warnings
|
Build
The process '/usr/bin/env' failed with exit code 1
|
|
Build:
Mathlib/Algebra/Order/SuccPred/TypeTags.lean#L6
unused import (use `lake exe shake --fix` to fix this, or `lake exe shake --update` to ignore)
|
|
Build:
Mathlib/Algebra/Order/SuccPred/TypeTags.lean#L7
import #[Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags] instead
|