Def CategoryTheory.Functor.constCompWhiskeringLeftIso

Modification history

2024-10-25 21:52
Mathlib/CategoryTheory/Functor/Const.lean
feat(CategoryTheory/KanExtension): Composing `lan` with `colim` (#17355)
Added CategoryTheory.Functor.constCompWhiskeringLeftIsoView on Github →