Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-09-02 14:19 227b6821

View on Github →

feat(category_theory): define iso.conj and friends (#1381)

feat(category_theory): define iso.conj and friends
Drop 2 @[simp] attributes

Estimated changes

Created src/category_theory/conj.lean

added theorem category_theory.functor.map_conj

added theorem category_theory.functor.map_conj_Aut

added theorem category_theory.functor.map_hom_congr

added def category_theory.iso.conj

added def category_theory.iso.conj_Aut

added theorem category_theory.iso.conj_Aut_apply

added theorem category_theory.iso.conj_Aut_gpow

added theorem category_theory.iso.conj_Aut_hom

added theorem category_theory.iso.conj_Aut_mul

added theorem category_theory.iso.conj_Aut_pow

added theorem category_theory.iso.conj_Aut_trans

added theorem category_theory.iso.conj_apply

added theorem category_theory.iso.conj_comp

added theorem category_theory.iso.conj_id

added theorem category_theory.iso.conj_pow

added def category_theory.iso.hom_congr

added theorem category_theory.iso.hom_congr_apply

added theorem category_theory.iso.hom_congr_comp

added theorem category_theory.iso.hom_congr_refl

added theorem category_theory.iso.hom_congr_symm

added theorem category_theory.iso.hom_congr_trans

added theorem category_theory.iso.refl_conj

added theorem category_theory.iso.self_symm_conj

added theorem category_theory.iso.symm_self_conj

added theorem category_theory.iso.trans_conj

added theorem category_theory.iso.trans_conj_Aut