Theorem CategoryTheory.LocalizerMorphism.Derives.isIso

Modification history

2025-11-16 19:50

Mathlib/CategoryTheory/Localization/DerivabilityStructure/Derives.lean

feat(CategoryTheory): deriving functors using a right derivability structure (#31400) …

Added CategoryTheory.LocalizerMorphism.Derives.isIso View on Github →