Commit 2023-02-18 18:53 876c87cd

View on Github →

feat: port CategoryTheory.Conj (#2316)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Conj.lean

added theorem CategoryTheory.Functor.map_conj

added theorem CategoryTheory.Functor.map_conjAut

added theorem CategoryTheory.Functor.map_homCongr

added def CategoryTheory.Iso.conj

added def CategoryTheory.Iso.conjAut

added theorem CategoryTheory.Iso.conjAut_apply

added theorem CategoryTheory.Iso.conjAut_hom

added theorem CategoryTheory.Iso.conjAut_mul

added theorem CategoryTheory.Iso.conjAut_pow

added theorem CategoryTheory.Iso.conjAut_trans

added theorem CategoryTheory.Iso.conjAut_zpow

added theorem CategoryTheory.Iso.conj_apply

added theorem CategoryTheory.Iso.conj_comp

added theorem CategoryTheory.Iso.conj_id

added theorem CategoryTheory.Iso.conj_pow

added def CategoryTheory.Iso.homCongr

added theorem CategoryTheory.Iso.homCongr_apply

added theorem CategoryTheory.Iso.homCongr_comp

added theorem CategoryTheory.Iso.homCongr_refl

added theorem CategoryTheory.Iso.homCongr_symm

added theorem CategoryTheory.Iso.homCongr_trans

added theorem CategoryTheory.Iso.refl_conj

added theorem CategoryTheory.Iso.self_symm_conj

added theorem CategoryTheory.Iso.symm_self_conj

added theorem CategoryTheory.Iso.trans_conj

added theorem CategoryTheory.Iso.trans_conjAut