-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | A library of constructive algebra.
--   
--   A library of algebra focusing mainly on commutative ring theory from a
--   constructive point of view.
--   
--   Classical structures are implemented without Noetherian assumptions.
--   This means that it is not assumed that all ideals are finitely
--   generated. For example, instead of principal ideal domains one gets
--   Bezout domains which are integral domains in which all finitely
--   generated ideals are principal (and not necessarily that all ideals
--   are principal).
@package constructive-algebra
@version 0.1.6


-- | Type level characters. Used for representing the variable name in
--   univariate polynomials.
module Algebra.TypeChar.Char
data A_
data B_
data C_
data D_
data E_
data F_
data G_
data H_
data I_
data J_
data K_
data L_
data M_
data N_
data O_
data P_
data Q_
data R_
data S_
data T_
data U_
data V_
data W_
data X_
data Y_
data Z_
data A
data B
data C
data D
data E
data F
data G
data H
data I
data J
data K
data L
data M
data N
data O
data P
data Q
data R
data S
data T
data U
data V
data W
data X
data Y
data Z
instance Show Z
instance Show Y
instance Show X
instance Show W
instance Show V
instance Show U
instance Show T
instance Show S
instance Show R
instance Show Q
instance Show P
instance Show O
instance Show N
instance Show M
instance Show L
instance Show K
instance Show J
instance Show I
instance Show H
instance Show G
instance Show F
instance Show E
instance Show D
instance Show C
instance Show B
instance Show A
instance Show Z_
instance Show Y_
instance Show X_
instance Show W_
instance Show V_
instance Show U_
instance Show T_
instance Show S_
instance Show R_
instance Show Q_
instance Show P_
instance Show O_
instance Show N_
instance Show M_
instance Show L_
instance Show K_
instance Show J_
instance Show I_
instance Show H_
instance Show G_
instance Show F_
instance Show E_
instance Show D_
instance Show C_
instance Show B_
instance Show A_


-- | The representation of the ring structure.
module Algebra.Structures.Ring

-- | Definition of rings.
class Ring a
(<+>) :: (Ring a) => a -> a -> a
(<*>) :: (Ring a) => a -> a -> a
neg :: (Ring a) => a -> a
zero :: (Ring a) => a
one :: (Ring a) => a

-- | Specification of rings. Test that the arguments satisfy the ring
--   axioms.
propRing :: (Ring a, Eq a) => a -> a -> a -> Property

-- | Subtraction
(<->) :: (Ring a) => a -> a -> a

-- | Exponentiation
(<^>) :: (Ring a) => a -> Integer -> a

-- | Multiply from left with an integer; n *&gt; x means x + x + ... + x, n
--   times.
(*>) :: (Ring a) => Integer -> a -> a
(<*) :: (Ring a) => a -> Integer -> a

-- | Summation
sumRing :: (Ring a) => [a] -> a

-- | Product
productRing :: (Ring a) => [a] -> a

module Algebra.Structures.CommutativeRing

-- | Definition of commutative rings.
class (Ring a) => CommutativeRing a

-- | Specification of commutative rings. Test that multiplication is
--   commutative and that it satisfies the ring axioms.
propCommutativeRing :: (CommutativeRing a, Eq a) => a -> a -> a -> Property


-- | Finitely generated ideals in commutative rings.
module Algebra.Ideal

-- | Ideals characterized by their list of generators.
data (CommutativeRing a) => Ideal a
Id :: [a] -> Ideal a

-- | The zero ideal.
zeroIdeal :: (CommutativeRing a) => Ideal a

-- | Test if an ideal is principal.
isPrincipal :: (CommutativeRing a) => Ideal a -> Bool
fromId :: (CommutativeRing a) => Ideal a -> [a]

-- | Evaluate the ideal at a certain point.
eval :: (CommutativeRing a) => a -> Ideal a -> a

-- | Addition of ideals.
addId :: (CommutativeRing a, Eq a) => Ideal a -> Ideal a -> Ideal a

-- | Multiplication of ideals.
mulId :: (CommutativeRing a, Eq a) => Ideal a -> Ideal a -> Ideal a

-- | Test if an operations compute the correct ideal. The 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
--   
--   This is used to check that the intersection computed is correct.
isSameIdeal :: (CommutativeRing a, Eq a) => (Ideal a -> Ideal a -> (Ideal a, [[a]], [[a]])) -> Ideal a -> Ideal a -> Bool

-- | Compute witnesses for two lists for the zero ideal. This is used when
--   computing the intersection of two ideals.
zeroIdealWitnesses :: (CommutativeRing a) => [a] -> [a] -> (Ideal a, [[a]], [[a]])
instance (CommutativeRing a, Arbitrary a, Eq a) => Arbitrary (Ideal a)
instance (CommutativeRing a, Show a) => Show (Ideal a)

module Algebra.Structures.StronglyDiscrete

-- | Strongly discrete rings
--   
--   A ring is called strongly discrete if ideal membership is decidable.
--   Nothing correspond to that x is not in the ideal and Just is the
--   witness. Examples include all Bezout domains and polynomial rings.
class (Ring a) => StronglyDiscrete a
member :: (StronglyDiscrete a) => a -> Ideal a -> Maybe [a]

-- | Test that the witness is actually a witness that the element is in the
--   ideal.
propStronglyDiscrete :: (CommutativeRing a, StronglyDiscrete a, Eq a) => a -> Ideal a -> Bool

module Algebra.Structures.IntegralDomain

-- | Definition of integral domains.
class (CommutativeRing a) => IntegralDomain a

-- | Specification of integral domains. Test that there are no
--   zero-divisors and that it satisfies the axioms of commutative rings.
propIntegralDomain :: (IntegralDomain a, Eq a) => a -> a -> a -> Property


-- | Representation of Euclidean domains. That is integral domains with an
--   Euclidean functions and decidable division.
module Algebra.Structures.EuclideanDomain

-- | Euclidean domains
--   
--   Given a and b compute (q,r) such that a = bq + r and r = 0 || d r &lt;
--   d b. Where d is the Euclidean function.
class (IntegralDomain a) => EuclideanDomain a
d :: (EuclideanDomain a) => a -> Integer
quotientRemainder :: (EuclideanDomain a) => a -> a -> (a, a)
propEuclideanDomain :: (EuclideanDomain a, Eq a) => a -> a -> a -> Property
modulo :: (EuclideanDomain a) => a -> a -> a
quotient :: (EuclideanDomain a) => a -> a -> a
divides :: (EuclideanDomain a, Eq a) => a -> a -> Bool

-- | The Euclidean algorithm for calculating the GCD of a and b.
euclidAlg :: (EuclideanDomain a, Eq a) => a -> a -> a

-- | Generalized Euclidean algorithm to compute GCD of a list of elements.
genEuclidAlg :: (EuclideanDomain a, Eq a) => [a] -> a

-- | Lowest common multiple, (a*b)/gcd(a,b).
lcmE :: (EuclideanDomain a, Eq a) => a -> a -> a

-- | Generalized lowest common multiple to compute lcm of a list of
--   elements.
genLcmE :: (EuclideanDomain a, Eq a) => [a] -> a

-- | The extended Euclidean algorithm.
--   
--   Computes x and y in ax + by = gcd(a,b).
extendedEuclidAlg :: (EuclideanDomain a, Eq a) => a -> a -> (a, a)

-- | Generalized extended Euclidean algorithm.
--   
--   Solves a_1 x_1 + ... + a_n x_n = gcd (a_1,...,a_n)
genExtendedEuclidAlg :: (EuclideanDomain a, Eq a) => [a] -> [a]


-- | A small simple matrix library.
module Algebra.Matrix

-- | Row vectors
newtype Vector r
Vec :: [r] -> Vector r
unVec :: Vector r -> [r]
lengthVec :: Vector r -> Int

-- | Matrices
newtype Matrix r
M :: [Vector r] -> Matrix r

-- | Construct a mxn matrix.
matrix :: [[r]] -> Matrix r
matrixToVector :: Matrix r -> Vector r
vectorToMatrix :: Vector r -> Matrix r
unMVec :: Matrix r -> [[r]]
unM :: Matrix r -> [Vector r]

-- | Construct a nxn identity matrix.
identity :: (IntegralDomain r) => Int -> Matrix r

-- | Matrix multiplication.
mulM :: (Ring r) => Matrix r -> Matrix r -> Matrix r

-- | Matrix addition.
addM :: (Ring r) => Matrix r -> Matrix r -> Matrix r

-- | Transpose a matrix.
transpose :: Matrix r -> Matrix r
isSquareMatrix :: Matrix r -> Bool

-- | Compute the dimension of a matrix.
dimension :: Matrix r -> (Int, Int)
instance (Eq r) => Eq (Matrix r)
instance (Eq r) => Eq (Vector r)
instance (Eq r, Arbitrary r, Ring r) => Arbitrary (Matrix r)
instance (Show r) => Show (Matrix r)
instance (Ring r, Arbitrary r, Eq r) => Arbitrary (Vector r)
instance (Show r) => Show (Vector r)


-- | Representation of coherent rings. Traditionally a ring is coherent if
--   every finitely generated ideal is finitely presented. This means that
--   it is possible to solve homogenous linear equations in them.
module Algebra.Structures.Coherent

-- | Definition of coherent rings.
--   
--   We say that R is coherent iff for any M, we can find L such that ML=0
--   and
--   
--   MX=0 &lt;-&gt; exists Y. X=LY
--   
--   that is, iff we can generate the solutions of any linear homogeous
--   system of equations.
--   
--   The main point here is that ML=0, it is not clear how to represent the
--   equivalence in Haskell. This would probably be possible in type
--   theory.
class (IntegralDomain a) => Coherent a
solve :: (Coherent a) => Vector a -> Matrix a
propCoherent :: (Coherent a, Eq a) => Vector a -> Bool

-- | Solves a system of equations.
solveMxN :: (Coherent a, Eq a) => Matrix a -> Matrix a

-- | Test that the solution of an MxN system is in fact a solution of the
--   system
propSolveMxN :: (Coherent a, Eq a) => Matrix a -> Bool

-- | Intersection computable -&gt; Coherence.
--   
--   Proof that if there is an algorithm to compute a f.g. set of
--   generators for the intersection of two f.g. ideals then the ring is
--   coherent.
--   
--   Takes the vector to solve, [x1,...,xn], and a function (int) that
--   computes the intersection of two ideals.
--   
--   If
--   
--   [ x_1, ..., x_n ] `int` [ y_1, ..., y_m ] = [ z_1, ..., z_l ]
--   
--   then int should give witnesses us and vs such that:
--   
--   z_k = n_k1 * x_1 + ... + u_kn * x_n
--   
--   = u_k1 * y_1 + ... + n_km * y_m
solveWithIntersection :: (IntegralDomain a, Eq a) => Vector a -> (Ideal a -> Ideal a -> (Ideal a, [[a]], [[a]])) -> Matrix a

-- | Strongly discrete coherent rings.
--   
--   If the ring is strongly discrete and coherent then we can solve
--   arbitrary equations of the type AX=b.
solveGeneralEquation :: (Coherent a, StronglyDiscrete a) => Vector a -> a -> Maybe (Matrix a)
propSolveGeneralEquation :: (Coherent a, StronglyDiscrete a, Eq a) => Vector a -> a -> Bool

-- | Solves general linear systems of the kind AX = B.
--   
--   A is given as a matrix and B is given as a row vector (it should be
--   column vector).
solveGeneral :: (Coherent a, StronglyDiscrete a, Eq a) => Matrix a -> Vector a -> Maybe (Matrix a, Matrix a)
propSolveGeneral :: (Coherent a, StronglyDiscrete a, Eq a) => Matrix a -> Vector a -> Property


-- | Prufer domains are non-Noetherian analogues of Dedekind domains. That
--   is integral domains in which every finitely generated ideal is
--   invertible. This implementation is mainly based on:
--   
--   http://hlombardi.free.fr/liens/salouThesis.pdf
module Algebra.Structures.PruferDomain

-- | Prufer domain
class (IntegralDomain a) => PruferDomain a
calcUVW :: (PruferDomain a) => a -> a -> (a, a, a)

-- | Property specifying that: au = bv and b(1-u) = aw
propCalcUVW :: (PruferDomain a, Eq a) => a -> a -> Bool
propPruferDomain :: (PruferDomain a, Eq a) => a -> a -> a -> Property

-- | Alternative characterization of Prufer domains, given a and b compute
--   u, v, w, t such that:
--   
--   ua = vb &amp;&amp; wa = tb &amp;&amp; u+t = 1
calcUVWT :: (PruferDomain a) => a -> a -> (a, a, a, a)
propCalcUVWT :: (PruferDomain a, Eq a) => a -> a -> Bool

-- | Go back to the original definition (yes the name is stupid :P).
fromUVWTtoUVW :: (PruferDomain a) => (a, a, a, a) -> (a, a, a)

-- | Compute a principal localization matrix for an ideal in a Prufer
--   domain.
computePLM_PD :: (PruferDomain a, Eq a) => Ideal a -> Matrix a

-- | Ideal inversion. Given I compute J such that IJ is principal. Uses the
--   principal localization matrix for the ideal.
invertIdeal :: (PruferDomain a, Eq a) => Ideal a -> Ideal a
intersectionPD :: (PruferDomain a, Eq a) => Ideal a -> Ideal a -> Ideal a

-- | Compute the intersection of I and J by:
--   
--   (I  J)(I + J) = IJ =&gt; (I  J)(I + J)(I + J)' = IJ(I + J)'
intersectionPDWitness :: (PruferDomain a, Eq a) => Ideal a -> Ideal a -> (Ideal a, [[a]], [[a]])

-- | Coherence of Prufer domains.
solvePD :: (PruferDomain a, Eq a) => Vector a -> Matrix a


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

-- | Bezout domains
--   
--   Compute a principal ideal from another ideal. Also give witness that
--   the principal ideal is equal to the first ideal.
--   
--   toPrincipal &lt;a_1,...,a_n&gt; = (&lt;a&gt;,u_i,v_i) where
--   
--   sum (u_i * a_i) = a
--   
--   a_i = v_i * a
class (IntegralDomain a) => BezoutDomain a
toPrincipal :: (BezoutDomain a) => Ideal a -> (Ideal a, [a], [a])
propBezoutDomain :: (BezoutDomain a, Eq a) => Ideal a -> a -> a -> a -> Property
dividesB :: (BezoutDomain a, Eq a) => a -> a -> Bool

-- | Intersection without witness.
intersectionB :: (BezoutDomain a, Eq a) => Ideal a -> Ideal a -> Ideal a

-- | Intersection of ideals with witness.
--   
--   If one of the ideals is the zero ideal then the intersection is the
--   zero ideal.
intersectionBWitness :: (BezoutDomain a, Eq a) => Ideal a -> Ideal a -> (Ideal a, [[a]], [[a]])

-- | Coherence of Bezout domains.
solveB :: (BezoutDomain a, Eq a) => Vector a -> Matrix a
instance [overlap ok] (BezoutDomain a, Eq a) => PruferDomain a
instance [overlap ok] (BezoutDomain a, Eq a) => StronglyDiscrete a
instance [overlap ok] (EuclideanDomain a, Eq a) => BezoutDomain a


-- | Specification of principal localization matrices used in the coherence
--   proof of Prufer domains.
module Algebra.PLM

-- | A principal localization matrix for an ideal (x1,...,xn) is a matrix
--   such that:
--   
--   <ul>
--   <li>The sum of the diagonal should equal 1.</li>
--   <li>For all i, j, l in {1..n}: a_lj * x_i = a_li * x_j</li>
--   </ul>
propPLM :: (CommutativeRing a, Eq a) => Ideal a -> Matrix a -> Bool

-- | Principal localization matrices for ideals are computable in Bezout
--   domains.
computePLM_B :: (BezoutDomain a, Eq a) => Ideal a -> Matrix a


-- | Greatest common divisor (GCD) domains.
--   
--   GCD domains are integral domains in which every pair of nonzero
--   elements have a greatest common divisor. They can also be
--   characterized as non-Noetherian analogues of unique factorization
--   domains.
module Algebra.Structures.GCDDomain

-- | GCD domains
class (IntegralDomain a) => GCDDomain a
gcd' :: (GCDDomain a) => a -> a -> (a, a, a)

-- | Specification of GCD domains. They are integral domains in which every
--   pair of nonzero elements have a greatest common divisor.
propGCDDomain :: (Eq a, GCDDomain a, Arbitrary a, Show a) => a -> a -> a -> Property
instance (BezoutDomain a) => GCDDomain a

module Algebra.Z

-- | Type synonym for integers.
type Z = Integer

-- | Definition of rings.
class Ring a
(<+>) :: (Ring a) => a -> a -> a
(<*>) :: (Ring a) => a -> a -> a
neg :: (Ring a) => a -> a
zero :: (Ring a) => a
one :: (Ring a) => a
instance Coherent Z
instance EuclideanDomain Z
instance IntegralDomain Z
instance CommutativeRing Z
instance Ring Z

module Algebra.Structures.Field

-- | Definition of fields.
class (IntegralDomain a) => Field a
inv :: (Field a) => a -> a

-- | Specification of fields. Test that the multiplicative inverses behave
--   as expected and that it satisfies the axioms of integral domains.
propField :: (Field a, Eq a) => a -> a -> a -> Property

-- | Division
(</>) :: (Field a) => a -> a -> a


-- | The field of fractions over a GCD domain. The reason that it is an GCD
--   domain is that we only want to work over reduced quotients.
module Algebra.Structures.FieldOfFractions

-- | Field of fractions
newtype (GCDDomain a) => FieldOfFractions a
F :: (a, a) -> FieldOfFractions a

-- | Embed a value in the field of fractions.
toFieldOfFractions :: (GCDDomain a) => a -> FieldOfFractions a

-- | Extract a value from the field of fractions. This is only possible if
--   the divisor is one.
fromFieldOfFractions :: (GCDDomain a, Eq a) => FieldOfFractions a -> a

-- | Reduce an element.
reduce :: (GCDDomain a, Eq a) => FieldOfFractions a -> FieldOfFractions a
instance (GCDDomain a, Eq a) => Field (FieldOfFractions a)
instance (GCDDomain a, Eq a) => IntegralDomain (FieldOfFractions a)
instance (GCDDomain a, Eq a) => CommutativeRing (FieldOfFractions a)
instance (GCDDomain a, Eq a) => Ring (FieldOfFractions a)
instance (GCDDomain a, Eq a) => Eq (FieldOfFractions a)
instance (GCDDomain a, Eq a, Arbitrary a) => Arbitrary (FieldOfFractions a)
instance (GCDDomain a, Show a, Eq a) => Show (FieldOfFractions a)


-- | Representation of rational numbers as the field of fractions of Z.
module Algebra.Q

-- | Q is the field of fractions of Z.
type Q = FieldOfFractions Z
toQ :: Z -> Q
toZ :: Q -> Z
instance Fractional Q
instance Num Q


-- | Univariate polynomials parametrised by the variable name.
module Algebra.UPoly

-- | Polynomials over a commutative ring, indexed by a phantom type x that
--   denote the name of the variable that the polynomial is over. For
--   example UPoly Q X_ is Q[x] and UPoly Q T_ is Q[t].
newtype (CommutativeRing r) => UPoly r x
UP :: [r] -> UPoly r x

-- | The degree of the polynomial.
deg :: (CommutativeRing r) => UPoly r x -> Integer

-- | Useful shorthand for Q[x].
type Qx = UPoly Q X_

-- | The variable x in Q[x].
x :: Qx

-- | Take a list and construct a polynomial by removing all zeroes in the
--   end.
toUPoly :: (CommutativeRing r, Eq r) => [r] -> UPoly r x

-- | Take an element of the ring and the degree of the desired monomial,
--   for example: monomial 3 7 = 3x^7
monomial :: (CommutativeRing r) => r -> Integer -> UPoly r x

-- | Compute the leading term of a polynomial.
lt :: (CommutativeRing r) => UPoly r x -> r

-- | Formal derivative of polynomials in k[x].
deriv :: (CommutativeRing r) => UPoly r x -> UPoly r x

-- | Square free decomposition of a polynomial.
sqfr :: (Num k, Field k) => UPoly k x -> UPoly k x

-- | Distinct power factorization, aka square free decomposition
sqfrDec :: (Num k, Field k) => UPoly k x -> [UPoly k x]
instance (Eq r) => Eq (UPoly r x)
instance (Ord r) => Ord (UPoly r x)
instance (Field k, Eq k) => EuclideanDomain (UPoly k x)
instance (CommutativeRing r, Eq r) => IntegralDomain (UPoly r x)
instance (CommutativeRing r, Eq r) => CommutativeRing (UPoly r x)
instance (Show r, Field r, Num r, Show x) => Num (UPoly r x)
instance (CommutativeRing r, Eq r) => Ring (UPoly r x)
instance (CommutativeRing r, Eq r, Arbitrary r) => Arbitrary (UPoly r x)
instance (CommutativeRing r, Eq r, Show r, Show x) => Show (UPoly r x)


-- | The field of rational functions is the field of fractions of k[x].
module Algebra.FieldOfRationalFunctions

-- | Field of rational functions.
type FieldOfRationalFunctions k x = FieldOfFractions (UPoly k x)

-- | The field of fraction of Q[x].
type QX = FieldOfRationalFunctions Q X_
toQX :: Qx -> QX
toQx :: QX -> Qx
instance (Show k, Field k, Num k, Show x) => Num (FieldOfRationalFunctions k x)


-- | Proof that Z[sqrt(-5)] is a Prufer domain. This implies that it is
--   possible to solve systems of equations over Z[sqrt(-5)].
module Algebra.ZSqrt5

-- | Z[sqrt(-5)] is a pair such that (a,b) = a + b*sqrt(-5)
newtype ZSqrt5
ZSqrt5 :: (Z, Z) -> ZSqrt5
instance Eq ZSqrt5
instance Ord ZSqrt5
instance Arbitrary ZSqrt5
instance Coherent ZSqrt5
instance PruferDomain ZSqrt5
instance IntegralDomain ZSqrt5
instance CommutativeRing ZSqrt5
instance Ring ZSqrt5
instance Show ZSqrt5


-- | The elliptic curve y^2 = 1 - x^4 in Q[x,y].
module Algebra.EllipticCurve

-- | The elliptic curve y^2=1-x^4 over Q[x,y].
newtype EllipticCurve
C :: (Qx, Qx) -> EllipticCurve
instance Eq EllipticCurve
instance Arbitrary EllipticCurve
instance Coherent EllipticCurve
instance PruferDomain EllipticCurve
instance IntegralDomain EllipticCurve
instance CommutativeRing EllipticCurve
instance Ring EllipticCurve
instance Show EllipticCurve


-- | Integers modulo n parametrised by the n. This also has type-level
--   primality testing used for instantiating integral domain and field
--   type classes. The primality testing is very slow, but it seem to be
--   working fine for relatively small numbers.
module Algebra.Zn

-- | The phantom type n represents which modulo to work in.
newtype Zn n
Zn :: Integer -> Zn n
instance Eq (Zn n)
instance Ord (Zn n)
instance (Pos x) => IsZero (x :* d) False
instance IsZero D9 False
instance IsZero D8 False
instance IsZero D7 False
instance IsZero D6 False
instance IsZero D5 False
instance IsZero D4 False
instance IsZero D3 False
instance IsZero D2 False
instance IsZero D1 False
instance IsZero D0 True
instance (Pred y z, Trich z D1 r1, Mod x y rest, IsZero rest b1, Not b1 b', Prime' x z r1 b2, And b' b2 b3) => Prime' x y GT b3
instance Prime' x D1 EQ True
instance (Sqrt x y, Trich y D1 r, Prime' x y r b) => Prime x b
instance (ExpBase y D2 square, Succ y y', Trich x square r, Sqrt' x y' r sqrt) => Sqrt' x y GT sqrt
instance (Pred y y') => Sqrt' x y EQ y'
instance (Sub y D2 y') => Sqrt' x y LT y'
instance (Nat x, Nat sqrt, Sqrt' x D1 GT sqrt) => Sqrt x sqrt
instance (Prime n True, Nat n) => Field (Zn n)
instance (Prime n True, Nat n) => IntegralDomain (Zn n)
instance (Nat n) => CommutativeRing (Zn n)
instance (Nat n) => Ring (Zn n)
instance (Nat n) => Arbitrary (Zn n)
instance (Nat n) => Num (Zn n)
instance Show (Zn n)