Nuprl Definition : int_mul_mon

<ℤ,*> ==  <ℤ, λx,y. (x =z y), λx,y. x ≤y, λx,y. (x y), 1, λx.x>



Definitions occuring in Statement :  le_int: i ≤j eq_int: (i =z j) lambda: λx.A[x] pair: <a, b> multiply: m natural_number: $n int:
Definitions occuring in definition :  int: eq_int: (i =z j) le_int: i ≤j multiply: m pair: <a, b> natural_number: $n lambda: λx.A[x]

Latex:
<\mBbbZ{},*>  ==    <\mBbbZ{},  \mlambda{}x,y.  (x  =\msubz{}  y),  \mlambda{}x,y.  x  \mleq{}z  y,  \mlambda{}x,y.  (x  *  y),  1,  \mlambda{}x.x>



Date html generated: 2016_05_15-PM-00_18_15
Last ObjectModification: 2015_09_23-AM-06_25_20

Theory : groups_1


Home Index