Def CategoryTheory.Subobject.homOfFactors

Modification history

2025-12-04 09:22

Mathlib/CategoryTheory/Subobject/FactorThru.lean

feat(CategoryTheory): Pullback of equalizer is an equalizer (#30120) …

Added CategoryTheory.Subobject.homOfFactors View on Github →