Theorem CategoryTheory.Arrow.isIso_of_isIso

Modification history

2026-06-22 18:03
Mathlib/CategoryTheory/Comma/Arrow.lean
chore(CategoryTheory/Comma/Arrow): use `to_dual` (#40862) …
Deleted CategoryTheory.Arrow.isIso_of_isIsoView on Github →
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_of_isIsoView on Github →