data.zmod.defs

# Definition of zmod n + basic results. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.lean. This file imports char_p/basic, which is an issue; all char_p instances create an algebra (zmod p) R instance; however, this instance may not be definitionally equal to other algebra instances (for example, galois_field also has an algebra instance as it is defined as a splitting_field). The way to fix this is to use the forgetful inheritance pattern, and make char_p carry the data of what the smul should be (so for example, the smul on the galois_field char_p instance should be equal to the smul from its splitting_field 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 char_p/basic to be able to import some part of zmod.

## Ring structure on fin n#

We define a commutative ring structure on fin n, but we do not register it as instance. 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.

@[protected, instance]
def fin.comm_semigroup (n : ) :

Multiplicative commutative semigroup structure on fin n.

Equations
@[protected, instance]
def fin.distrib (n : ) :
Equations
@[protected, instance]
def fin.comm_ring (n : ) [ne_zero n] :

Commutative ring structure on fin n.

Equations
@[protected, instance]
def fin.has_distrib_neg (n : ) :

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

Equations
def zmod  :

The integers modulo n : ℕ.

Equations
Instances for zmod
@[protected, instance]
Equations
@[protected, instance]
def zmod.has_repr (n : ) :
Equations
@[protected, instance]
def zmod.fintype (n : ) [ne_zero n] :
Equations
@[protected, instance]
@[simp]
theorem zmod.card (n : ) [fintype (zmod n)] :
@[protected, instance]
def zmod.comm_ring (n : ) :
Equations
@[protected, instance]
def zmod.inhabited (n : ) :
Equations