Theorem CategoryTheory.IsHomLift.comp_lift_id_left'

Modification history

2024-06-18 06:24
Mathlib/CategoryTheory/FiberedCategory/HomLift.lean
feat(FiberedCategory/Cartesian): define cartesian morphisms (#13393) …
Added CategoryTheory.IsHomLift.comp_lift_id_left'View on Github →