constructive-algebra-0.1.3: A library of constructive algebra.



Representation of Bezout domains. That is non-Noetherian analogues of principal ideal domains. This means that all finitely generated ideals are principal.



class IntegralDomain a => BezoutDomain a whereSource

Bezout domains

Compute 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


toPrincipal :: Ideal a -> (Ideal a, [a], [a])Source


propBezoutDomain :: (BezoutDomain a, Eq a) => Ideal a -> a -> a -> a -> PropertySource

dividesB :: (BezoutDomain a, Eq a) => a -> a -> BoolSource

intersectionB :: (BezoutDomain a, Eq a) => Ideal a -> Ideal a -> Ideal aSource

Intersection without witness.

intersectionBWitness :: (BezoutDomain a, Eq a) => Ideal a -> Ideal a -> (Ideal a, [[a]], [[a]])Source

Intersection of ideals with witness.

If one of the ideals is the zero ideal then the intersection is the zero ideal.

solveB :: (BezoutDomain a, Eq a) => Vector a -> Matrix aSource

Coherence of Bezout domains.