Mathlib Changelog
Changelog
About
Github
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