Theorem CategoryTheory.CartesianMonoidalCategory.whiskerLeft_toUnit_comp_rightUnitor_hom

Modification history