Commit 2026-03-25 18:13 93b67f8e

View on Github →

chore(Algebra/Order/Nonneg/Lattice): clean up instances (#37157) Use inferInstanceAs for instances on { x : α // a ≤ x } inherited from (Ici a).

Estimated changes