mathlib3 documentation

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]

Multiplicative commutative semigroup structure on fin n.

Equations
@[protected, instance]

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

Equations
@[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