Commit 2025-02-01 11:21 19755f8f

View on Github →

feat(CategoryTheory): transfer being iso along an iso in the arrow category (#21310) This is probably the minmal set of necessary lemmas

Estimated changes

Modified Mathlib/CategoryTheory/Comma/Arrow.lean

added theorem CategoryTheory.Arrow.isIso_hom_iff_isIso_hom_of_isIso

added theorem CategoryTheory.Arrow.isIso_hom_iff_isIso_of_isIso

added theorem CategoryTheory.Arrow.isIso_iff_isIso_of_isIso

added theorem CategoryTheory.Arrow.isIso_of_isIso