Commit 2025-02-23 15:47 f7a295f8

View on Github →

feat(CategoryTheory): IsPullback version of 'pullback of iso is iso' (#22211)

Estimated changes

Modified Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean

added theorem CategoryTheory.IsPullback.isIso_fst_of_isIso

added theorem CategoryTheory.IsPullback.isIso_snd_of_isIso

added theorem CategoryTheory.IsPushout.isIso_inl_of_isIso

added theorem CategoryTheory.IsPushout.isIso_inr_of_isIso