Theorem CategoryTheory.CartesianMonoidalCategory.whiskerRight_toUnit_comp_leftUnitor_hom

Modification history