# 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`

.

## Equations

- Fin.instCommSemigroup n = let src := inferInstanceAs (Mul (Fin n)); CommSemigroup.mk (_ : ∀ (a b : Fin n), a * b = b * a)

Note this is more general than `Fin.instCommRing`

as it applies (vacuously) to `Fin 0`

too.

## Equations

- ZMod.decidableEq x = match x with | 0 => inferInstanceAs (DecidableEq ℤ) | Nat.succ n => inferInstanceAs (DecidableEq (Fin (n + 1)))

## Equations

- ZMod.fintype x✝ = match x✝, x with | 0, h => (_ : False).elim | Nat.succ n, x => Fin.fintype (n + 1)

## Equations

- ZMod.commRing n = CommRing.mk (_ : ∀ (a b : ZMod n), a * b = b * a)

## Equations

- ZMod.inhabited n = { default := 0 }