Inductive CategoryTheory.IsHomLiftAux

Modification history

2025-11-02 18:17

Mathlib/CategoryTheory/FiberedCategory/HomLift.lean

chore(CategoryTheory/FiberedCategory/HomLift): Unify IsHomLift and IsHomLiftAux (#31125) …

Deleted CategoryTheory.IsHomLiftAux View on Github →

2024-06-04 16:04

Mathlib/CategoryTheory/FiberedCategory/HomLift.lean

feat(FiberedCategory/HomLift): definition of IsHomLift (#12978) …

Added CategoryTheory.IsHomLiftAux View on Github →