mathlib3
b98d8408
- feat(category_theory/category): initialize simps (#7605)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
4 years ago
feat(category_theory/category): initialize simps (#7605) Initialize `@[simps]` so that it works better for `category`. It just makes the names of the generated lemmas shorter. Add `@[simps]` to product categories.
Author
fpvandoorn
Parents
9084a3c7
Loading