algebra-4.2: Constructive abstract algebra

Numeric.Domain.Euclidean

Documentation

class (Ring r, DecidableZero r, DecidableUnits r, Domain r) => Euclidean r where Source

Minimal complete definition

Methods

splitUnit :: r -> (r, r) Source

`splitUnit r` calculates its leading unit and normal form.

`let (u, n) = splitUnit r in r == u * n && fst (splitUnit n) == one && isUnit u`

degree :: r -> Maybe Natural Source

Euclidean (degree) function on `r`.

divide infix 7 Source

Arguments

 :: r elements divided by -> r divisor -> (r, r) quotient and remin

Division algorithm. `a divide b` calculates quotient and reminder of `a` divided by `b`.

`let (q, r) = divide a p in p*q + r == a && degree r < degree q`

quot :: r -> r -> r infixl 7 Source

rem :: r -> r -> r infixl 7 Source

gcd :: r -> r -> r Source

`gcd a b` calculates greatest common divisor of `a` and `b`.

euclid :: r -> r -> [(r, r, r)] Source

Extended euclidean algorithm.

`euclid f g == xs ==> all (\(r, s, t) -> r == f * s + g * t) xs`

Instances

 Euclidean Integer

prs :: Euclidean r => r -> r -> [(r, r, r)] Source

normalize :: Euclidean r => r -> r Source

gcd' :: Euclidean r => [r] -> r Source

Arguments

 :: Euclidean r => [(r, r)] List of `(m_i, v_i)` -> r `f` with `f` = `v_i` (mod `v_i`)