Def CategoryTheory.Limits.liftPrecomp

Modification history

2025-12-04 09:22

Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean

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

Added CategoryTheory.Limits.liftPrecomp View on Github →