Commit 2025-01-24 22:55 afdba6f8
View on Github →refactor: make LinearOrderedCommMonoidWithZero extend OrderBot (#19193)
Currently, the following fails:
import Mathlib
variable {α : Type*} [LinearOrderedCommGroupWithZero α]
#synth OrderBot α
/-
failed to synthesize
OrderBot α
Additional diagnostic information may be available using the `set_option diagnostics true` command.
-/