Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-06 08:30 56ed5d78

View on Github →

feat(category_theory/adjunction): mates (#5599) Adds some results on the calculus of mates.

Estimated changes

Created src/category_theory/adjunction/mates.lean

added def category_theory.transfer_nat_trans

added theorem category_theory.transfer_nat_trans_counit

added def category_theory.transfer_nat_trans_self

added theorem category_theory.transfer_nat_trans_self_comm

added theorem category_theory.transfer_nat_trans_self_comp

added theorem category_theory.transfer_nat_trans_self_counit

added theorem category_theory.transfer_nat_trans_self_id

added def category_theory.transfer_nat_trans_self_of_iso

added theorem category_theory.transfer_nat_trans_self_symm_comm

added theorem category_theory.transfer_nat_trans_self_symm_comp

added theorem category_theory.transfer_nat_trans_self_symm_id

added def category_theory.transfer_nat_trans_self_symm_of_iso

added theorem category_theory.unit_transfer_nat_trans

added theorem category_theory.unit_transfer_nat_trans_self