Library mathcomp.algebra.zmodp

Definition of the additive group and ring Zp, represented as 'I_p Definitions: From fintype.v: 'I_p == the subtype of integers less than p, taken here as the type of the integers mod p. This file: inZp == the natural projection from nat into the integers mod p, represented as 'I_p. Here p is implicit, but MUST be of the form n.+1. The operations: Zp0 == the identity element for addition Zp1 == the identity element for multiplication, and a generator of additive group Zp_opp == inverse function for addition Zp_add == addition Zp_mul == multiplication Zp_inv == inverse function for multiplication Note that while 'I_n.+1 has canonical finZmodType and finGroupType structures, only 'I_n.+2 has a canonical ring structure (it has, in fact, a canonical finComUnitRing structure), and hence an associated multiplicative unit finGroupType. To mitigate the issues caused by the trivial "ring" (which is, indeed is NOT a ring in the ssralg/finalg formalization), we define additional notation: 'Z_p == the type of integers mod (max p 2); this is always a proper ring, by constructions. Note that 'Z_p is provably equal to 'I_p if p > 1, and convertible to 'I_p if p is of the form n.+2. Zp p == the subgroup of integers mod (max p 1) in 'Z_p; this is thus all of 'Z_p if p > 1, and else the trivial group. units_Zp p == the group of all units of 'Z_p -- i.e., the group of (multiplicative) automorphisms of Zp p. We show that Zp and units_Zp are abelian, and compute their orders. We use a similar technique to represent the prime fields: 'F_p == the finite field of integers mod the first prime divisor of maxn p 2. This is provably equal to 'Z_p and 'I_p if p is provably prime, and indeed convertible to the above if p is a concrete prime such as 2, 5 or 23. Note finally that due to the canonical structures it is possible to use 0%R instead of Zp0, and 1%R instead of Zp1 (for the latter, p must be of the form n.+2, and 1%R : nat will simplify to 1%N).

Mod p arithmetic on the finite set {0, 1, 2, ..., p - 1}

Standard injection; val (inZp i) = i %% p

Operations

Additive group structure.

Ring operations

We redefine fintype.ord1 to specialize it with 0 instead of ord0 since 'I_n is now canonically a zmodType

Field structure for primes.