mathlib
60c2b68c - feat(data/sigma/order): The lexicographical order has a bot/top (#10905)

Commit
3 years ago
feat(data/sigma/order): The lexicographical order has a bot/top (#10905) Also fix localized instances declarations. They weren't using fully qualified names and I had forgotten `sigma.lex.linear_order`.
Author
Parents
Loading