Def CategoryTheory.Functor.FullyFaithful.compYonedaCompWhiskeringLeftMaxRight

Modification history

2026-07-15 16:59
Mathlib/CategoryTheory/Yoneda.lean
chore: delete deprecated declarations to the end of 2025 (#41178) …
Deleted CategoryTheory.Functor.FullyFaithful.compYonedaCompWhiskeringLeftMaxRightView on Github →
2026-05-29 13:23
Mathlib/CategoryTheory/Yoneda.lean
chore: bump toolchain to v4.31.0-rc1 (#39980)
Added CategoryTheory.Functor.FullyFaithful.compYonedaCompWhiskeringLeftMaxRightView on Github →
2026-05-17 20:27
Mathlib/CategoryTheory/Yoneda.lean
chore: remove declarations deprecated between 2021-05-15 and 2025-11-15 (#39405) …
Deleted CategoryTheory.Functor.FullyFaithful.compYonedaCompWhiskeringLeftMaxRightView on Github →
2024-11-02 10:16
Mathlib/CategoryTheory/Yoneda.lean
feat: even more natural versions of `FullyFaithful.homEquiv` (#18524) …
Added CategoryTheory.Functor.FullyFaithful.compYonedaCompWhiskeringLeftMaxRightView on Github →