# Definition of `ZMod n`

+ basic results. #

This file provides the basic details of `ZMod n`

, including its commutative ring structure.

## Implementation details #

This used to be inlined into `Data.ZMod.Basic`

. This file imports `CharP.Basic`

, which is an
issue; all `CharP`

instances create an `Algebra (ZMod p) R`

instance; however, this instance may
not be definitionally equal to other `Algebra`

instances (for example, `GaloisField`

also has an
`Algebra`

instance as it is defined as a `SplittingField`

). The way to fix this is to use the
forgetful inheritance pattern, and make `CharP`

carry the data of what the `smul`

should be (so
for example, the `smul`

on the `GaloisField`

`CharP`

instance should be equal to the `smul`

from
its `SplittingField`

structure); there is only one possible `ZMod p`

algebra for any `p`

, so this
is not an issue mathematically. For this to be possible, however, we need `CharP.Basic`

to be
able to import some part of `ZMod`

.

## Ring structure on `Fin n`

#

We define a commutative ring structure on `Fin n`

.
Afterwards, when we define `ZMod n`

in terms of `Fin n`

, we use these definitions
to register the ring structure on `ZMod n`

as type class instance.

Multiplicative commutative semigroup structure on `Fin n`

.

Note this is more general than `Fin.instCommRing`

as it applies (vacuously) to `Fin 0`

too.