Def CategoryTheory.effectiveEpiStructOfRegularEpi

Modification history

2025-12-01 06:24
Mathlib/CategoryTheory/Limits/Shapes/RegularMono.lean
refactor(Category Theory): change `RegularMono`/`Epi` from class to structure (#32154) …
Modified CategoryTheory.effectiveEpiStructOfRegularEpiView on Github →
2025-11-21 13:53
Mathlib/CategoryTheory/EffectiveEpi/RegularEpi.lean
feat(CategoryTheory): effective epi implies strong epi (#31860) …
Modified CategoryTheory.effectiveEpiStructOfRegularEpiView on Github →
2024-03-19 13:54
Mathlib/CategoryTheory/EffectiveEpi/RegularEpi.lean
chore(CategoryTheory): split the file `CategoryTheory/Sites/EffectiveEpimorphic/Basic.lean` (#11458) …
Modified CategoryTheory.effectiveEpiStructOfRegularEpiView on Github →
2023-11-20 12:33
Mathlib/CategoryTheory/Sites/EffectiveEpimorphic.lean
fix(CategoryTheory): remove unnecessary noncomputable modifier (#8528) …
Added CategoryTheory.effectiveEpiStructOfRegularEpiView on Github →