Conj

📁 Source: Mathlib/CategoryTheory/Conj.lean

Statistics

Metric	Count
Definitions conj, conjAut, Conj	3
Theorems map_conj, map_conjAut, conjAut_apply, conjAut_hom, conjAut_mul, conjAut_pow, conjAut_trans, conjAut_zpow, conj_apply, conj_comp, conj_id, conj_pow, refl_conj, self_symm_conj, symm_self_conj, trans_conj, trans_conjAut	17
Total	20

CategoryTheory.Functor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_conj 📖	mathematical	—	map DFunLike.coe MulEquiv CategoryTheory.End CategoryTheory.Category.toCategoryStruct CategoryTheory.End.mul EquivLike.toFunLike MulEquiv.instEquivLike CategoryTheory.Iso.conj obj mapIso	—	map_homCongr
map_conjAut 📖	mathematical	—	mapIso DFunLike.coe MulEquiv CategoryTheory.Aut MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Aut.instGroup EquivLike.toFunLike MulEquiv.instEquivLike CategoryTheory.Iso.conjAut obj	—	CategoryTheory.Iso.ext map_conj

CategoryTheory.Iso

Definitions

Name	Category	Theorems
conj 📖	CompOp	15 math math: refl_conj, conj_pow, CategoryTheory.Functor.map_conj, FGModuleCat.Iso.conj_eq_conj, SemimoduleCat.Iso.conj_eq_conj, symm_self_conj, self_symm_conj, conjAut_hom, ModuleCat.Iso.conj_eq_conj, conj_id, trans_conj, conj_comp, Action.Iso.conj_ρ, FGModuleCat.Iso.conj_hom_eq_conj, conj_apply
conjAut 📖	CompOp	8 math math: conjAut_apply, conjAut_mul, trans_conjAut, CategoryTheory.Functor.map_conjAut, conjAut_hom, conjAut_zpow, conjAut_pow, conjAut_trans

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
conjAut_apply 📖	mathematical	—	DFunLike.coe MulEquiv CategoryTheory.Aut MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Aut.instGroup EquivLike.toFunLike MulEquiv.instEquivLike conjAut trans symm	—	CategoryTheory.Aut.ext
conjAut_hom 📖	mathematical	—	hom DFunLike.coe MulEquiv CategoryTheory.Aut MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Aut.instGroup EquivLike.toFunLike MulEquiv.instEquivLike conjAut CategoryTheory.End CategoryTheory.Category.toCategoryStruct CategoryTheory.End.mul conj	—	—
conjAut_mul 📖	mathematical	—	DFunLike.coe MulEquiv CategoryTheory.Aut MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Aut.instGroup EquivLike.toFunLike MulEquiv.instEquivLike conjAut	—	map_mul MonoidHomClass.toMulHomClass MulEquivClass.instMonoidHomClass MulEquiv.instMulEquivClass
conjAut_pow 📖	mathematical	—	DFunLike.coe MulEquiv CategoryTheory.Aut MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Aut.instGroup EquivLike.toFunLike MulEquiv.instEquivLike conjAut Monoid.toNatPow	—	map_pow MulEquivClass.instMonoidHomClass MulEquiv.instMulEquivClass
conjAut_trans 📖	mathematical	—	DFunLike.coe MulEquiv CategoryTheory.Aut MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Aut.instGroup EquivLike.toFunLike MulEquiv.instEquivLike conjAut trans	—	conjAut_mul
conjAut_zpow 📖	mathematical	—	DFunLike.coe MulEquiv CategoryTheory.Aut MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Aut.instGroup EquivLike.toFunLike MulEquiv.instEquivLike conjAut DivInvMonoid.toZPow	—	map_zpow MulEquivClass.instMonoidHomClass MulEquiv.instMulEquivClass
conj_apply 📖	mathematical	—	DFunLike.coe MulEquiv CategoryTheory.End CategoryTheory.Category.toCategoryStruct CategoryTheory.End.mul EquivLike.toFunLike MulEquiv.instEquivLike conj CategoryTheory.CategoryStruct.comp inv hom	—	—
conj_comp 📖	mathematical	—	DFunLike.coe MulEquiv CategoryTheory.End CategoryTheory.Category.toCategoryStruct CategoryTheory.End.mul EquivLike.toFunLike MulEquiv.instEquivLike conj CategoryTheory.CategoryStruct.comp	—	map_mul MonoidHomClass.toMulHomClass MulEquivClass.instMonoidHomClass MulEquiv.instMulEquivClass
conj_id 📖	mathematical	—	DFunLike.coe MulEquiv CategoryTheory.End CategoryTheory.Category.toCategoryStruct CategoryTheory.End.mul EquivLike.toFunLike MulEquiv.instEquivLike conj CategoryTheory.CategoryStruct.id	—	map_one MonoidHomClass.toOneHomClass MulEquivClass.instMonoidHomClass MulEquiv.instMulEquivClass
conj_pow 📖	mathematical	—	DFunLike.coe MulEquiv CategoryTheory.End CategoryTheory.Category.toCategoryStruct CategoryTheory.End.mul EquivLike.toFunLike MulEquiv.instEquivLike conj Monoid.toNatPow CategoryTheory.End.monoid	—	MonoidHom.map_pow
refl_conj 📖	mathematical	—	DFunLike.coe MulEquiv CategoryTheory.End CategoryTheory.Category.toCategoryStruct CategoryTheory.End.mul EquivLike.toFunLike MulEquiv.instEquivLike conj refl	—	conj_apply refl_inv refl_hom CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id
self_symm_conj 📖	mathematical	—	DFunLike.coe MulEquiv CategoryTheory.End CategoryTheory.Category.toCategoryStruct CategoryTheory.End.mul EquivLike.toFunLike MulEquiv.instEquivLike conj symm	—	symm_self_conj
symm_self_conj 📖	mathematical	—	DFunLike.coe MulEquiv CategoryTheory.End CategoryTheory.Category.toCategoryStruct CategoryTheory.End.mul EquivLike.toFunLike MulEquiv.instEquivLike conj symm	—	trans_conj self_symm_id refl_conj
trans_conj 📖	mathematical	—	DFunLike.coe MulEquiv CategoryTheory.End CategoryTheory.Category.toCategoryStruct CategoryTheory.End.mul EquivLike.toFunLike MulEquiv.instEquivLike conj trans	—	homCongr_trans
trans_conjAut 📖	mathematical	—	DFunLike.coe MulEquiv CategoryTheory.Aut MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Aut.instGroup EquivLike.toFunLike MulEquiv.instEquivLike conjAut trans	—	conjAut_apply trans_assoc

Quandle

Definitions

Name	Category	Theorems
Conj 📖	CompOp	4 math math: Rack.envelAction_prop, conj_swap, Rack.toEnvelGroup.univ, conj_act_eq_conj

---

← Back to Index