Commit 2024-03-25 19:47 e80129c5

View on Github →

feat: some missing API for the category of elements (#11483) The most significant change is the introduction of the simp lemma map_snd.

Estimated changes

Modified Mathlib/CategoryTheory/Elements.lean

added def CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalenceFunctorProj

added def CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalenceInverseπ

added theorem CategoryTheory.CategoryOfElements.map_snd