WhoCites
Definitions
IteratedBinops
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /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 /sfa/Nuprl/Shared/Xindentation_hack_doc.html
WhoCites
Definitions
IteratedBinops
Sections
DiscrMathExt
Doc
x:A. f(u,x) = x & f(x,u) = xf:(A
AA), u:A. is_ident(A; f; u) 
Propx:A. f(u,x) = x & f(x,u) = xf:(AAA), u:A. is_ident(A; f; u) Prop
