WhoCites
Definitions
IteratedBinops
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Commutativity of a function
Who Cites is
commutative?
is_commutative
Def is_commutative(
A
;
x
,
z
.
f
(
x
;
z
)) ==
x
,
z
:
A
.
f
(
x
;
z
) =
f
(
z
;
x
)
A
Thm*
f
:(
A
A
A
). is_commutative(
A
;
x
,
z
.
f
(
x
,
z
))
Prop
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
WhoCites
Definitions
IteratedBinops
Sections
DiscrMathExt
Doc
x,z:A. f(x;z) = f(z;x) 
Af:(A
AA). is_commutative(A; x,z.f(x,z)) Propx,z:A. f(x;z) = f(z;x) Af:(AAA). is_commutative(A; x,z.f(x,z)) Prop
