Opposite

📁 Source: Mathlib/GroupTheory/Congruence/Opposite.lean

Statistics

Metric	Count
Definitions op, orderIsoOp, unop, op, orderIsoOp, unop	6
Theorems orderIsoOp_apply, orderIsoOp_symm_apply, orderIsoOp_apply, orderIsoOp_symm_apply	4
Total	10

AddCon

Definitions

Name	Category	Theorems
op 📖	CompOp	1 math math: orderIsoOp_apply
orderIsoOp 📖	CompOp	2 math math: orderIsoOp_apply, orderIsoOp_symm_apply
unop 📖	CompOp	1 math math: orderIsoOp_symm_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
orderIsoOp_apply 📖	mathematical	—	DFunLike.coe RelIso AddCon AddOpposite AddOpposite.instAdd instLE RelIso.instFunLike orderIsoOp op	—	—
orderIsoOp_symm_apply 📖	mathematical	—	DFunLike.coe RelIso AddCon AddOpposite AddOpposite.instAdd instLE RelIso.instFunLike RelIso.symm orderIsoOp unop	—	—

Con

Definitions

Name	Category	Theorems
op 📖	CompOp	1 math math: orderIsoOp_apply
orderIsoOp 📖	CompOp	2 math math: orderIsoOp_symm_apply, orderIsoOp_apply
unop 📖	CompOp	1 math math: orderIsoOp_symm_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
orderIsoOp_apply 📖	mathematical	—	DFunLike.coe RelIso Con MulOpposite MulOpposite.instMul instLE RelIso.instFunLike orderIsoOp op	—	—
orderIsoOp_symm_apply 📖	mathematical	—	DFunLike.coe RelIso Con MulOpposite MulOpposite.instMul instLE RelIso.instFunLike RelIso.symm orderIsoOp unop	—	—

---

← Back to Index