Theorem CategoryTheory.Equivalence.Mon_.rightUnitor_inv_hom

Modification history