OpClass

📁 Source: Mathlib/Logic/OpClass.lean

Statistics

Metric	Count
Definitions IsSymmOp, LeftCommutative, RightCommutative	3
Theorems flip_eq, symm_op, left_comm, right_comm, instLeftCommutativeOfCommutativeOfAssociative, instLeftCommutativeOfRightCommutative, instRightCommutativeOfCommutativeOfAssociative, instRightCommutativeOfLeftCommutative, isSymmOp_of_isCommutative	9
Total	12

IsSymmOp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
flip_eq 📖	—	—	—	—	symm_op
symm_op 📖	—	—	—	—	—

LeftCommutative

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
left_comm 📖	—	—	—	—	—

RightCommutative

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
right_comm 📖	—	—	—	—	—

(root)

Definitions

Name	Category	Theorems
IsSymmOp 📖	CompData	2 math math: isSymmOp_of_isCommutative, List.instIsSymmOpZipWith
LeftCommutative 📖	CompData	4 math math: instLeftCommutativeOfRightCommutative, max_left_commutative, min_left_commutative, instLeftCommutativeOfCommutativeOfAssociative
RightCommutative 📖	CompData	3 math math: instRightCommutativeOfCommutativeOfAssociative, Multiset.instRightCommutativeErase, instRightCommutativeOfLeftCommutative

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instLeftCommutativeOfCommutativeOfAssociative 📖	mathematical	—	LeftCommutative	—	—
instLeftCommutativeOfRightCommutative 📖	mathematical	—	LeftCommutative	—	RightCommutative.right_comm
instRightCommutativeOfCommutativeOfAssociative 📖	mathematical	—	RightCommutative	—	—
instRightCommutativeOfLeftCommutative 📖	mathematical	—	RightCommutative	—	LeftCommutative.left_comm
isSymmOp_of_isCommutative 📖	mathematical	—	IsSymmOp	—	—

---

← Back to Index