Theorem CategoryTheory.Arrow.isIso_hom_iff_isIso_of_isIso

Modification history

2025-02-01 11:21
Mathlib/CategoryTheory/Comma/Arrow.lean
feat(CategoryTheory): transfer being iso along an iso in the arrow category (#21310) …
Added CategoryTheory.Arrow.isIso_hom_iff_isIso_of_isIsoView on Github →