- class Ring a => StronglyDiscrete a where
- propStronglyDiscrete :: (CommutativeRing a, StronglyDiscrete a, Eq a) => a -> Ideal a -> Bool

# Documentation

class Ring a => StronglyDiscrete a whereSource

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.

(BezoutDomain a, Eq a) => StronglyDiscrete a | Strongly discreteness for Bezout domains Given x, compute as such that x = sum (a_i * x_i) |

propStronglyDiscrete :: (CommutativeRing a, StronglyDiscrete a, Eq a) => a -> Ideal a -> BoolSource

Test that the witness is actually a witness that the element is in the ideal.