Theorem CategoryTheory.ExponentialIdeal.mk'

Modification history

2025-03-02 21:26

Mathlib/CategoryTheory/Closed/Ideal.lean

feat(CategoryTheory/Abelian): the inverse image of a Serre class by an exact functor (#22342) …

Modified CategoryTheory.ExponentialIdeal.mk'View on Github →

2023-06-27 08:51

Mathlib/CategoryTheory/Closed/Ideal.lean

feat: port CategoryTheory.Closed.Ideal (#4951)

Added CategoryTheory.ExponentialIdeal.mk'View on Github →