mathlib3
e17aab9b - chore(*): cleanup unneeded uses of by_cases across the library

Commit

4 years ago

chore(*): cleanup unneeded uses of by_cases across the library

Author

alexjbest

alexjbest

Parents

Loading