úÎ@ã<}>      !"#$%&'()*+,-./01 2 3 4 5 6 7 8 9 : ; < = Definition of rings.  Addition Multiplication Compute additive inverse The additive identity The multiplicative identity >?@ABCDEISpecification of rings. Test that the arguments satisfy the ring axioms.  Subtraction  Summation Product Exponentiation      !Definition of commutative rings. F ASpecification of commutative rings. Test that multiplication is 4 commutative and that it satisfies the ring axioms.     2Ideals characterized by their list of generators. The zero ideal. Test if an ideal is principal. 'Evaluate the ideal at a certain point. Addition of ideals. Multiplication of ideals. 2Test if an operations compute the correct ideal. DThe operation should give a witness that the comuted ideal contains the same elements. If [ x_1, ..., x_n ] `op` [ y_1, ..., y_m ] = [ z_1, ..., z_l ] "Then the witness should give that $z_k = a_k1 * x_1 + ... + a_kn * x_n $ = b_k1 * y_1 + ... + b_km * y_m AThis is used to check that the intersection computed is correct. GCompute witnesses for two lists for the zero ideal. This is used when + computing the intersection of two ideals.   Strongly discrete rings EA ring is called strongly discrete if ideal membership is decidable. K Nothing correspond to that x is not in the ideal and Just is the witness. ; Examples include all Bezout domains and polynomial rings. HTest that the witness is actually a witness that the element is in the  ideal.  Definition of integral domains. GHSpecification of integral domains. Test that there are no zero-divisors 8 and that it satisfies the axioms of commutative rings.  Euclidean domains BGiven a and b compute (q,r) such that a = bq + r and r = 0 || d r < d b. $ Where d is the Euclidean function. HI !"#<The Euclidean algorithm for calculating the GCD of a and b. $FGeneralized Euclidean algorithm to compute GCD of a list of elements. %Lowest common multiple, (a*b)/ gcd(a,b). &IGeneralized lowest common multiple to compute lcm of a list of elements. '#The extended Euclidean algorithm. (Computes x and y in ax + by = gcd(a,b). J(*Generalized extended Euclidean algorithm. 3Solves a_1 x_1 + ... + a_n x_n = gcd (a_1,...,a_n) K  !"#$%&'(  !"#$%&'(  !"#$%&'()Bezout domains ICompute a principal ideal from another ideal. Also give witness that the . principal ideal is equal to the first ideal.  toPrincipal <a_1,...,a_n> = (< a>,u_i,v_i)  where sum (u_i * a_i) = a a_i = v_i * a *LM+,%Intersection of ideals with witness. JIf one of the ideals is the zero ideal then the intersection is the zero  ideal. -Intersection without witness. N)Strongly discreteness for Bezout domains 2Given x, compute as such that x = sum (a_i * x_i) )*+,-)*+-,)**+,-. GCD domains /6Compute gcd(a,b) = (g,x,y) such that g = gcd(a,b) and  a = gx  b = gy  and a, b /= 0 O0HSpecification of GCD domains. They are integral domains in which every : pair of nonzero elements have a greatest common divisor. ./0./0.//0 1Type synonym for integers. PQRS111 2Definition of fields. 3T4JSpecification of fields. Test that the multiplicative inverses behave as @ expected and that it satisfies the axioms of integral domains. 5 Division  2345234523345 6Field of fractions 78)Embed a value in the field of fractions. 9JExtract a value from the field of fractions. This is only possible if the  divisor is one. :Reduce an element. U6789:6789:67789: ;"Q is the field of fractions of Z. <=;<=;<=;<=V  !"#$%&'()*+,-./0123456789:;<= > ? @ A B C D E F G H I JKLMNOPQRSTUVWXYZ[\ ] ^ _ ` a bcconstructive-algebra-0.1.1Algebra.Structures.Ring"Algebra.Structures.CommutativeRing Algebra.Ideal#Algebra.Structures.StronglyDiscrete!Algebra.Structures.IntegralDomain"Algebra.Structures.EuclideanDomainAlgebra.Structures.BezoutDomainAlgebra.Structures.GCDDomain Algebra.ZAlgebra.Structures.Field#Algebra.Structures.FieldOfFractions Algebra.QRing<+><*>negzeroonepropRing<->sumRing productRing<^>CommutativeRingpropCommutativeRingIdealId zeroIdeal isPrincipalfromIdevaladdIdmulId isSameIdealzeroIdealWitnessesStronglyDiscretememberpropStronglyDiscreteIntegralDomainpropIntegralDomainEuclideanDomaindquotientRemainderpropEuclideanDomainmoduloquotientdivides euclidAlg genEuclidAlglcmEgenLcmEextendedEuclidAlggenExtendedEuclidAlg BezoutDomain toPrincipalpropBezoutDomainintersectionBWitness intersectionB GCDDomaingcd' propGCDDomainZFieldinv propFieldFieldOfFractionsFtoFieldOfFractionsfromFieldOfFractionsreduceQtoQtoZ propAddAssocpropAddIdentity propAddInv propAddComm propMulAssoc propRightDist propLeftDistpropMulIdentity propMulCommpropZeroDivisorspropD propQuotRempropExtendedEuclidAlgpropGenExtEuclidAlgpropToPrincipalpropIsSameIdeal$fStronglyDiscreteapropGCDpropIntegralDomainZpropEuclideanDomainZpropBezoutDomainZpropStronglyDiscreteZ propMulInv propReduce