Commit 2023-02-24 08:05 de57375e

View on Github →

feat: Port CategoryTheory.Adjunction.Mates (#2455)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Adjunction/Mates.lean

added def CategoryTheory.transferNatTrans

added def CategoryTheory.transferNatTransSelf

added theorem CategoryTheory.transferNatTransSelf_adjunction_id

added theorem CategoryTheory.transferNatTransSelf_adjunction_id_symm

added theorem CategoryTheory.transferNatTransSelf_comm

added theorem CategoryTheory.transferNatTransSelf_comp

added theorem CategoryTheory.transferNatTransSelf_counit

added theorem CategoryTheory.transferNatTransSelf_id

added theorem CategoryTheory.transferNatTransSelf_of_iso

added theorem CategoryTheory.transferNatTransSelf_symm_comm

added theorem CategoryTheory.transferNatTransSelf_symm_comp

added theorem CategoryTheory.transferNatTransSelf_symm_id

added theorem CategoryTheory.transferNatTransSelf_symm_of_iso

added theorem CategoryTheory.transferNatTrans_counit

added theorem CategoryTheory.unit_transferNatTrans

added theorem CategoryTheory.unit_transferNatTransSelf