Commit 2025-07-19 15:53 4fba5e6e

View on Github →

feat: Over.map of an iso is an equivalence (#27139) From Toric

Estimated changes

Modified Mathlib/CategoryTheory/Comma/Over/Basic.lean

modified def CategoryTheory.Over.mapIso

modified theorem CategoryTheory.Over.mapIso_functor

modified theorem CategoryTheory.Over.mapIso_inverse

modified def CategoryTheory.Under.mapIso

modified theorem CategoryTheory.Under.mapIso_functor

modified theorem CategoryTheory.Under.mapIso_inverse