Nuprl Definition : ring_term_value

ring_term_value(f;t) ==
  int_term_ind(t;
               itermConstant(n)⇒ int-to-ring(r;n);
               itermVar(v)⇒ f v;
               itermAdd(a,b)⇒ av,bv.av +r bv;
               itermSubtract(a,b)⇒ av,bv.av +r (-r bv);
               itermMultiply(a,b)⇒ av,bv.av * bv;
               itermMinus(a)⇒ av.-r av) 


Definitions occuring in Statement :  int-to-ring: int-to-ring(r;n),  rng_times: *,  rng_minus: -r,  rng_plus: +r,  int_term_ind: int_term_ind,  infix_ap: x f y,  apply: f a
Definitions occuring in definition :  int_term_ind: int_term_ind,  int-to-ring: int-to-ring(r;n),  rng_plus: +r,  infix_ap: x f y,  rng_times: *,  apply: f a,  rng_minus: -r
FDL editor aliases :  ring_term_value
Latex:
ring\_term\_value(f;t)  ==
    int\_term\_ind(t;
                              itermConstant(n){}\mRightarrow{}  int-to-ring(r;n);
                              itermVar(v){}\mRightarrow{}  f  v;
                              itermAdd(a,b){}\mRightarrow{}  av,bv.av  +r  bv;
                              itermSubtract(a,b){}\mRightarrow{}  av,bv.av  +r  (-r  bv);
                              itermMultiply(a,b){}\mRightarrow{}  av,bv.av  *  bv;
                              itermMinus(a){}\mRightarrow{}  av.-r  av) 


Date html generated: 2018_05_21-PM-03_15_23
Last ObjectModification: 2018_01_25-AM-10_55_17

Theory : rings_1


Home Index