Structures · Logic and sets

IsSymmOp

IsSymmOp op where op : α → α → β says that op is a symmetric operation, i.e. op a b = op b a. It is the natural generalisation of Std.Commutative (β = α) and IsSymm (β = Prop).

Defined in

Mathlib.Logic.OpClass

Shape

One type argument · adds symm_op