Commit 2025-04-09 15:42 548ae365
View on Github →chore(CategoryTheory/Equivalence): simp lemmas for co/unit naturality (#23724)
Add simp lemmas for naturality of the co/units of an equivalence, and use them to remove some erw's.
chore(CategoryTheory/Equivalence): simp lemmas for co/unit naturality (#23724)
Add simp lemmas for naturality of the co/units of an equivalence, and use them to remove some erw's.