Nuprl Definition : int_op
i x(op;id;inv) e == if 0 ≤z i then i x(op;id) e else inv -i x(op;id) e fi
Definitions occuring in Statement :
nat_op: n x(op;id) e,
le_int: i ≤z j,
ifthenelse: if b then t else f fi ,
apply: f a,
minus: -n,
natural_number: $n
Definitions occuring in definition :
ifthenelse: if b then t else f fi ,
le_int: i ≤z j,
natural_number: $n,
apply: f a,
nat_op: n x(op;id) e,
minus: -n
Latex:
i x(op;id;inv) e == if 0 \mleq{}z i then i x(op;id) e else inv -i x(op;id) e fi
Date html generated:
2016_05_15-PM-00_15_27
Last ObjectModification:
2015_09_23-AM-06_25_00
Theory : groups_1
Home
Index