Commit 2c3e688
committed
feat(CategoryTheory/Comma/Basic): use
This PR continues tagging things about `Comma` with `to_dual`.
This PR also expands the `to_dual_name_hint` syntax so that you can give multiple name hints with a single command, instead of having to repeat the command.
This PR adds `CategoryTheory.Comma.map_obj_hom'`, the dual of `CategoryTheory.Comma.map_obj_hom`.to_dual more (leanprover-community#40355)1 parent 28c4b7f commit 2c3e688
4 files changed
Lines changed: 81 additions & 134 deletions
File tree
- MathlibTest/Attribute
- Mathlib
- CategoryTheory/Comma
- Order/Interval/Set
- Tactic/Translate
0 commit comments