Documentation

greatest common divisor.

Properties For all a and b in N holds:

1. gcd a b == gcd b a.
2. gcd a b == 0 if and only if a == 0 and b == 0.
4. gcd a 0 == a.
4. gcd a 1 == 1.
5. gcd a b * lcm a b == a * b.

greatest common divisor of the given list.

Note gcds [] == 0.

least common multiple.

Properties For all a and b in N holds:

1. lcm a b == lcm b a.
2. lcm a b == 1 if and only if a == 1 and b == 1.
3. lcm a 0 == 0.
4. lcm a 1 == a.
5. gcd a b * lcm a b == a * b.

least common multiple of the given list.

Property lcms [] == 1.

extended euclidean algorithm to determine the greatest cowmon divisor.

Properties (g,s,t) = euclid a b then

1. g is the greatest common divisor of a and b.
2. g == s * a + t * b.

extended modulo in Z according to N.

Property For all z and n holds

1. mod0 z 0 == z.
2. if 0 < n than mod0 z n == mod z (inj n).

extended division in Z by a dividend in N.

Properties For all z and n holds:

1. 0 // 0 == 1.
2. if z /= 0 then z // 0 == 0.
3. if 0 < n then z // n == div z n.
4. z == (z // n) * inj n + mod0 z n.