Theorem CategoryTheory.PrelaxFunctor.map₂Iso_eqToIso

Modification history

2025-09-01 13:46
Mathlib/CategoryTheory/Bicategory/Functor/Prelax.lean
chore(CategoryTheory/Bicategory): move `map₂_eqToHom` earlier in the import graph (#28287) …
Added CategoryTheory.PrelaxFunctor.map₂Iso_eqToIsoView on Github →