End

📁 Source: Mathlib/Algebra/Order/Group/End.lean

Statistics

Metric	Count
Definitions instMonoid, instMonoid, instGroup	3
Theorems coe_mul, coe_one, mul_apply, mul_def, one_apply, one_def, coe_mul, coe_one, mul_apply, mul_def, one_apply, one_def, apply_inv_self, coe_mul, coe_one, inv_apply_self, mul_apply, mul_def, one_apply, one_def	20
Total	23

RelEmbedding

Definitions

Name	Category	Theorems
instMonoid 📖	CompOp	8 math math: coe_one, smul_def, one_apply, mul_def, apply_faithfulSMul, mul_apply, coe_mul, one_def

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_mul 📖	mathematical	—	DFunLike.coe RelEmbedding instFunLike MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass instMonoid	—	—
coe_one 📖	mathematical	—	DFunLike.coe RelEmbedding instFunLike MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass instMonoid	—	—
mul_apply 📖	mathematical	—	DFunLike.coe RelEmbedding instFunLike MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass instMonoid	—	—
mul_def 📖	mathematical	—	RelEmbedding MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass instMonoid trans	—	—
one_apply 📖	mathematical	—	DFunLike.coe RelEmbedding instFunLike MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass instMonoid	—	—
one_def 📖	mathematical	—	RelEmbedding MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass instMonoid refl	—	—

RelHom

Definitions

Name	Category	Theorems
instMonoid 📖	CompOp	8 math math: one_def, one_apply, mul_apply, coe_one, smul_def, mul_def, apply_faithfulSMul, coe_mul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_mul 📖	mathematical	—	DFunLike.coe RelHom instFunLike MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass instMonoid	—	—
coe_one 📖	mathematical	—	DFunLike.coe RelHom instFunLike MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass instMonoid	—	—
mul_apply 📖	mathematical	—	DFunLike.coe RelHom instFunLike MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass instMonoid	—	—
mul_def 📖	mathematical	—	RelHom MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass instMonoid comp	—	—
one_apply 📖	mathematical	—	DFunLike.coe RelHom instFunLike MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass instMonoid	—	—
one_def 📖	mathematical	—	RelHom MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass instMonoid id	—	—

RelIso

Definitions

Name	Category	Theorems
instGroup 📖	CompOp	15 math math: one_apply, smul_def, Function.sSup_div_semiconj, mul_apply, one_def, CircleDeg1Lift.coe_toOrderIso_symm, CircleDeg1Lift.coe_toOrderIso_inv, coe_one, coe_mul, inv_apply_self, apply_faithfulSMul, CircleDeg1Lift.coe_toOrderIso, mul_def, apply_inv_self, Flag.coe_smul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_inv_self 📖	mathematical	—	DFunLike.coe RelIso instFunLike DivInvMonoid.toInv Group.toDivInvMonoid instGroup	—	apply_symm_apply
coe_mul 📖	mathematical	—	DFunLike.coe RelIso instFunLike MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instGroup	—	—
coe_one 📖	mathematical	—	DFunLike.coe RelIso instFunLike MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instGroup	—	—
inv_apply_self 📖	mathematical	—	DFunLike.coe RelIso instFunLike DivInvMonoid.toInv Group.toDivInvMonoid instGroup	—	symm_apply_apply
mul_apply 📖	mathematical	—	DFunLike.coe RelIso instFunLike MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instGroup	—	—
mul_def 📖	mathematical	—	RelIso MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instGroup trans	—	—
one_apply 📖	mathematical	—	DFunLike.coe RelIso instFunLike MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instGroup	—	—
one_def 📖	mathematical	—	RelIso MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instGroup refl	—	—

---

← Back to Index