Theorem CategoryTheory.Functor.isIso_of_isRightDerivedFunctor_of_inverts

Modification history

2025-11-16 19:50
Mathlib/CategoryTheory/Functor/Derived/PointwiseRightDerived.lean
feat(CategoryTheory): deriving functors using a right derivability structure (#31400) …
Added CategoryTheory.Functor.isIso_of_isRightDerivedFunctor_of_invertsView on Github →