Commit 2024-11-02 10:16 9a15d111

View on Github →

feat: even more natural versions of FullyFaithful.homEquiv (#18524) A natural follow-up to #17450.

Estimated changes

Modified Mathlib/CategoryTheory/Yoneda.lean

added def CategoryTheory.Functor.FullyFaithful.compYonedaCompWhiskeringLeft

added def CategoryTheory.Functor.FullyFaithful.compYonedaCompWhiskeringLeftMaxRight