Theorem HomotopicalAlgebra.PathObject.ofFactorizationData_p

Modification history

2025-08-11 11:23
Mathlib/AlgebraicTopology/ModelCategory/PathObject.lean
feat(AlgebraicTopology): path objects in model categories (#26958) …
Added HomotopicalAlgebra.PathObject.ofFactorizationData_pView on Github →