Def CategoryTheory.Yoneda.preimageIso

Modification history

2024-05-30 18:46

Mathlib/CategoryTheory/Yoneda.lean

refactor(CategoryTheory): the structure Functor.FullyFaithful (#12929) …

Deleted CategoryTheory.Yoneda.preimageIso View on Github →

2024-04-27 09:23

Mathlib/CategoryTheory/Yoneda.lean

chore(CategoryTheory): make `Functor.Full` a Prop (#12449) …

Added CategoryTheory.Yoneda.preimageIso View on Github →