This singleton data type establishes a correspondence between a modulo m on type level and its factorisation on term level.

Create a singleton from a type-level positive modulo m, passed in a constraint.

>>> :set -XDataKinds
>>> sfactors :: SFactors Integer 13
SFactors {unSFactors = [(Prime 13,1)]}

Create a singleton from factors of m. Factors must be distinct, as in output of factorise.

>>> import Math.NumberTheory.Primes
>>> someSFactors (factorise 98)
SFactors {unSFactors = [(Prime 2,1),(Prime 7,2)]}

Factors of m.

Convert a singleton to a proof that m is known. Usage example:

toModulo :: SFactors Integer m -> Natural
toModulo t = case proofFromSFactors t of Sub Dict -> natVal t

This singleton data type establishes a correspondence between a modulo m on type level and a cyclic group of the same order on term level.

Create a singleton from a type-level positive modulo m, passed in a constraint.

>>> :set -XDataKinds
>>> import Data.Maybe
>>> cyclicGroup :: Maybe (CyclicGroup Integer 169)
Just (CGOddPrimePower' (Prime 13) 2)

>>> :set -XTypeOperators -XNoStarIsType
>>> import GHC.TypeNats
>>> sfactorsToCyclicGroup (sfactors :: SFactors Integer 4)
Just CG4'
>>> sfactorsToCyclicGroup (sfactors :: SFactors Integer (2 * 13 ^ 3))
Just (CGDoubleOddPrimePower' (Prime 13) 3)
>>> sfactorsToCyclicGroup (sfactors :: SFactors Integer  (4 * 13))
Nothing

Create a singleton from factors. Factors must be distinct, as in output of factorise.

Similar to cyclicGroupFromFactors . factorise, but much faster, because it but performes only one primality test instead of full factorisation.

Convert a cyclic group to a proof that m is known. Usage example:

toModulo :: CyclicGroup Integer m -> Natural
toModulo t = case proofFromCyclicGroup t of Sub Dict -> natVal t

Unidirectional pattern for residues modulo 2.

Unidirectional pattern for residues modulo 4.

Unidirectional pattern for residues modulo p^k for odd prime p.

Unidirectional pattern for residues modulo 2p^k for odd prime p.

Invert sfactorsToCyclicGroup.

>>> import Data.Maybe
>>> cyclicGroupToSFactors (fromJust (sfactorsToCyclicGroup (sfactors :: SFactors Integer 4)))
SFactors {unSFactors = [(Prime 2,2)]}

Check whether a multiplicative group of residues, characterized by its modulo, is cyclic and, if yes, return its form.

>>> :set -XTypeOperators -XNoStarIsType
>>> import GHC.TypeNats
>>> sfactorsToCyclicGroup (sfactors :: SFactors Integer 4)
Just CG4'
>>> sfactorsToCyclicGroup (sfactors :: SFactors Integer (2 * 13 ^ 3))
Just (CGDoubleOddPrimePower' (Prime 13) 3)
>>> sfactorsToCyclicGroup (sfactors :: SFactors Integer  (4 * 13))
Nothing

Wrapper to hide an unknown type-level natural.