mathlib
26c838fc
- refactor(data/real/ennreal): remove ordered sub simp lemmas (#9902)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
4 years ago
refactor(data/real/ennreal): remove ordered sub simp lemmas (#9902) * They are now simp lemmas in `algebra/order/sub` * Squeeze some simps
Author
fpvandoorn
Parents
dc1484e4
Loading