Opposite

📁 Source: Mathlib/Algebra/Regular/Opposite.lean

Statistics

Metric	Count
Definitions	0
Theorems op, unop, op, unop, op, unop, op, unop, op, unop, op, unop, isAddLeftRegular_op, isAddLeftRegular_unop, isAddRegular_op, isAddRegular_unop, isAddRightRegular_op, isAddRightRegular_unop, isLeftRegular_op, isLeftRegular_unop, isRegular_op, isRegular_unop, isRightRegular_op, isRightRegular_unop	24
Total	24

IsAddLeftRegular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
op 📖	mathematical	IsAddRightRegular	IsAddLeftRegular AddOpposite AddOpposite.instAdd AddOpposite.op	—	isAddLeftRegular_op
unop 📖	mathematical	IsAddRightRegular AddOpposite AddOpposite.instAdd	IsAddLeftRegular AddOpposite.unop	—	isAddLeftRegular_unop

IsAddRegular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
op 📖	mathematical	IsAddRegular	AddOpposite AddOpposite.instAdd AddOpposite.op	—	isAddRegular_op
unop 📖	mathematical	IsAddRegular AddOpposite AddOpposite.instAdd	AddOpposite.unop	—	isAddRegular_unop

IsAddRightRegular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
op 📖	mathematical	IsAddLeftRegular	IsAddRightRegular AddOpposite AddOpposite.instAdd AddOpposite.op	—	isAddRightRegular_op
unop 📖	mathematical	IsAddLeftRegular AddOpposite AddOpposite.instAdd	IsAddRightRegular AddOpposite.unop	—	isAddRightRegular_unop

IsLeftRegular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
op 📖	mathematical	IsRightRegular	IsLeftRegular MulOpposite MulOpposite.instMul MulOpposite.op	—	isLeftRegular_op
unop 📖	mathematical	IsRightRegular MulOpposite MulOpposite.instMul	IsLeftRegular MulOpposite.unop	—	isLeftRegular_unop

IsRegular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
op 📖	mathematical	IsRegular	MulOpposite MulOpposite.instMul MulOpposite.op	—	isRegular_op
unop 📖	mathematical	IsRegular MulOpposite MulOpposite.instMul	MulOpposite.unop	—	isRegular_unop

IsRightRegular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
op 📖	mathematical	IsLeftRegular	IsRightRegular MulOpposite MulOpposite.instMul MulOpposite.op	—	isRightRegular_op
unop 📖	mathematical	IsLeftRegular MulOpposite MulOpposite.instMul	IsRightRegular MulOpposite.unop	—	isRightRegular_unop

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isAddLeftRegular_op 📖	mathematical	—	IsAddLeftRegular AddOpposite AddOpposite.instAdd AddOpposite.op IsAddRightRegular	—	Equiv.comp_injective Equiv.injective_comp
isAddLeftRegular_unop 📖	mathematical	—	IsAddLeftRegular AddOpposite.unop IsAddRightRegular AddOpposite AddOpposite.instAdd	—	isAddRightRegular_op
isAddRegular_op 📖	mathematical	—	IsAddRegular AddOpposite AddOpposite.instAdd AddOpposite.op	—	isAddRegular_iff isAddLeftRegular_op isAddRightRegular_op
isAddRegular_unop 📖	mathematical	—	IsAddRegular AddOpposite.unop AddOpposite AddOpposite.instAdd	—	isAddRegular_op
isAddRightRegular_op 📖	mathematical	—	IsAddRightRegular AddOpposite AddOpposite.instAdd AddOpposite.op IsAddLeftRegular	—	Equiv.comp_injective Equiv.injective_comp
isAddRightRegular_unop 📖	mathematical	—	IsAddRightRegular AddOpposite.unop IsAddLeftRegular AddOpposite AddOpposite.instAdd	—	isAddLeftRegular_op
isLeftRegular_op 📖	mathematical	—	IsLeftRegular MulOpposite MulOpposite.instMul MulOpposite.op IsRightRegular	—	Equiv.comp_injective Equiv.injective_comp
isLeftRegular_unop 📖	mathematical	—	IsLeftRegular MulOpposite.unop IsRightRegular MulOpposite MulOpposite.instMul	—	isRightRegular_op
isRegular_op 📖	mathematical	—	IsRegular MulOpposite MulOpposite.instMul MulOpposite.op	—	—
isRegular_unop 📖	mathematical	—	IsRegular MulOpposite.unop MulOpposite MulOpposite.instMul	—	isRegular_op
isRightRegular_op 📖	mathematical	—	IsRightRegular MulOpposite MulOpposite.instMul MulOpposite.op IsLeftRegular	—	Equiv.comp_injective Equiv.injective_comp
isRightRegular_unop 📖	mathematical	—	IsRightRegular MulOpposite.unop IsLeftRegular MulOpposite MulOpposite.instMul	—	isLeftRegular_op

---

← Back to Index