Theorem CategoryTheory.HasExactLimitsOfShape.of_codomain_equivalence

Modification history

2026-10-30 15:08
Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Basic.lean
chore(CategoryTheory): deprecate `leftExactFunctor` (#45418) …
Modified CategoryTheory.HasExactLimitsOfShape.of_codomain_equivalenceView on Github →
2025-12-13 14:21
Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Basic.lean
chore: use `Category*` everywhere (#32842) …
Modified CategoryTheory.HasExactLimitsOfShape.of_codomain_equivalenceView on Github →
2024-12-16 16:45
Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Basic.lean
feat(CategoryTheory/Abelian/GrothendieckAxioms): introduce Grothendieck categories (#18510) …
Added CategoryTheory.HasExactLimitsOfShape.of_codomain_equivalenceView on Github →