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. 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
instance Fin.instDistrib (n : ) :

Commutative ring structure on Fin n.

Equations
instance Fin.instCommRing (n : ) [NeZero n] :

Commutative ring structure on Fin n.

Equations

Note this is more general than Fin.instCommRing as it applies (vacuously) to Fin 0 too.

Equations
def ZMod :
Type

The integers modulo n : ℕ.

Equations
Instances For
    instance ZMod.repr (n : ) :
    Equations
    instance ZMod.fintype (n : ) [NeZero n] :
    Equations
    @[simp]
    theorem ZMod.card (n : ) [Fintype (ZMod n)] :
    instance ZMod.commRing (n : ) :
    Equations
    instance ZMod.inhabited (n : ) :
    Equations