Commit 2023-09-28 22:53 4b23a873

View on Github →

chore(CategoryTheory/Adjunction/Basic): missing dsimp lemmas (#7361)

Estimated changes

Modified Mathlib/CategoryTheory/Adjunction/Basic.lean

deleted theorem CategoryTheory.Equivalence.asEquivalence_toAdjunction_counit

deleted theorem CategoryTheory.Equivalence.asEquivalence_toAdjunction_unit

Modified Mathlib/CategoryTheory/Monoidal/NaturalTransformation.lean