# Documentation

Mathlib.Data.ZMod.Defs

# 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. Afterwords, 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
instance Fin.instCommRingFin (n : ) [inst : ] :

Commutative ring structure on Fin n.

Equations
• = let src := ; let src_1 := ; let src_2 := ; CommRing.mk (_ : ∀ (a b : Fin n), a * b = b * a)
def ZMod :

The integers modulo n : ℕ.

Equations
instance ZMod.decidableEq (n : ) :
Equations
instance ZMod.repr (n : ) :
Equations
• = match x with | 0 => id inferInstance | => id inferInstance
instance ZMod.fintype (n : ) [inst : ] :
Equations
Equations
@[simp]
theorem ZMod.card (n : ) [inst : Fintype (ZMod n)] :
instance ZMod.commRing (n : ) :
Equations
instance ZMod.inhabited (n : ) :
Equations
• = { default := 0 }