Algebra.Structures.StronglyDiscrete
- 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 euclidean domains and the polynomial ring.
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.