Theorem OrderHom.uliftLeftMap_uliftRightMap_eq

Modification history

2025-10-28 23:08
Mathlib/Order/Hom/Basic.lean
feat(AlgebraicTopology): the homotopy category functor preserves products (#25780) …
Added OrderHom.uliftLeftMap_uliftRightMap_eqView on Github →