WhoCites
Definitions
IteratedBinops
Sections
DiscrMathExt
Search
Doc
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
(
u
is an identity element for operation
f
on
A
)
Who Cites is
ident?
is_ident
Def is_ident(
A
;
f
;
u
) ==
x
:
A
.
f
(
u
,
x
) =
x
&
f
(
x
,
u
) =
x
Thm*
f
:(
A
A
A
),
u
:
A
. is_ident(
A
;
f
;
u
)
Prop
About:
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
WhoCites
Definitions
IteratedBinops
Sections
DiscrMathExt
Search
Doc
x:A. f(u,x) = x & f(x,u) = x
A
Prop
