Commit 2023-02-13 06:51 5bf726d3

View on Github →

feat: port CategoryTheory.Functor.InvIsos (#2237)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Functor/InvIsos.lean

added def CategoryTheory.compInvIso

added def CategoryTheory.invCompIso

added def CategoryTheory.isoCompInv

added def CategoryTheory.isoInvComp