Journal of Formalized Mathematics
Volume 9, 1997
University of Bialystok
Copyright (c) 1997
Association of Mizar Users
The Correctness of the Generic Algorithms of Brown and Henrici
Concerning Addition and Multiplication in Fraction Fields

Christoph Schwarzweller

University of T\"ubingen,
T\"ubingen
Summary.

We prove the correctness of the generic algorithms of Brown and Henrici
concerning addition and multiplication in fraction fields of gcddomains.
For that we first prove some basic facts about divisibility in integral
domains and introduce the concept of amplesets. After that we are able to
define gcddomains and to prove the theorems of Brown and Henrici which are
crucial for the correctness of the algorithms. In the last section we
define Mizar functions mirroring their input/output behaviour and prove
properties of these functions that ensure the correctness of the algorithms.
MML Identifier:
GCD_1
The terminology and notation used in this paper have been
introduced in the following articles
[3]
[5]
[4]
[2]
[1]

Basics

AmpleSets

GCDDomains

The Theorems of Brown and Henrici

Correctness of the Algorithms
Bibliography
 [1]
Eugeniusz Kusak, Wojciech Leonczuk, and Michal Muzalewski.
Abelian groups, fields and vector spaces.
Journal of Formalized Mathematics,
1, 1989.
 [2]
Michal Muzalewski.
Construction of rings and left, right, and bimodules over a ring.
Journal of Formalized Mathematics,
2, 1990.
 [3]
Andrzej Trybulec.
Tarski Grothendieck set theory.
Journal of Formalized Mathematics,
Axiomatics, 1989.
 [4]
Wojciech A. Trybulec.
Vectors in real linear space.
Journal of Formalized Mathematics,
1, 1989.
 [5]
Zinaida Trybulec.
Properties of subsets.
Journal of Formalized Mathematics,
1, 1989.
Received June 16, 1997
[
Download a postscript version,
MML identifier index,
Mizar home page]