(96) |

(97) |

(98) |

(99) |

(100) |

(101) |

(102) |

(103) |

If then is the inverse of . Conversely if is invertible there exists such that

(104) |

That is there exists such that . If and could be divided by an element which is not a unit then we would be led to a contradiction ( ). Hence .

ResidueClassRing(R:EuclideanDomain, p:R): Ring with { class: R -> %; sample: % -> R; } == R add { Rep == R; import from R; 1: % == per(1); 0: % == per(0); zero?(x:%): Boolean == zero?(rep(x)); (x:%) = (y:%) : Boolean == zero?(x-y); one?(x:%): Boolean == x = 1; class(a:R):% == { (q,r) := divide(a,p); per(r); } sample(x:%): R == rep(x); (x:%) + (y:%) : % == class(rep(x) + rep(y)); -(x:%) : % == class(-rep(x)); (x:%) * (y:%) : % == class(rep(x) * rep(y)); (n:Integer) * (x:%): % == class(n * rep(x)); (x:%) ^ (n:NonNegativeInteger) : % == class(rep(x) ^ n); recip(x:%): Partial(%) == { import from Partial(%); (u,v,g) := extendedEuclidean(rep(x),p); h?: Partial(R) := recip(g); failed? h? => failed(); h: R := retract(h?); [class(h * u)]; } }

(105) |

(106) |

(107) |

(108) |

(109) |

*
*

2008-01-07