Commit 2019-11-04 15:02 ee5b38df
View on Github →feat(simps): allow the user to specify the projections (#1630)
- feat(simps): allow the user to specify the projections Also add option to shorten generated lemma names Add the attribute to more places in the category_theory library The projection lemmas of inl_ and inr_ are now called inl__obj and similar
- use simps partially in limits/cones and whiskering
- revert whiskering
- rename last_name to short_name
- Update src/category_theory/products/basic.lean
- Update src/category_theory/limits/cones.lean Co-Authored-By: Scott Morrison scott@tqft.net
- Update src/category_theory/products/associator.lean Co-Authored-By: Scott Morrison scott@tqft.net
- Update src/data/string/defs.lean Co-Authored-By: Scott Morrison scott@tqft.net
- clarify is_eta_expansion docstrings