chore: generalise more lemmas from LinearOrderedField to `GroupWith…
#10793
Annotations
1 error and 2 warnings
|
check for unused imports
The process '/usr/bin/env' failed with exit code 1
|
|
check for unused imports:
Mathlib/Algebra/Order/Field/Pointwise.lean#L7
unused import (use `lake exe shake --fix` to fix this, or `lake exe shake --update` to ignore)
|
|
check for unused imports:
Mathlib/Algebra/Order/Field/Pointwise.lean#L8
import #[Mathlib.Algebra.Order.Field.Defs] instead
|
Loading