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.Lemmas, 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.Lemmas 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.

instance Fin.instCommSemigroup (n : ℕ) : CommSemigroup (Fin n)

Multiplicative commutative semigroup structure on Fin n.

Equations

• Fin.instCommSemigroup n = { toMul := inferInstanceAs (Mul (Fin n)), mul_assoc := ⋯, mul_comm := ⋯ }

instance Fin.instDistrib (n : ℕ) : Distrib (Fin n)

Distributive structure on Fin n.

Equations

• Fin.instDistrib n = { toMul := (Fin.instCommSemigroup n).toMul, toAdd := (Fin.addCommSemigroup n).toAdd, left_distrib := ⋯, right_distrib := ⋯ }

instance Fin.instNonUnitalCommRing (n : ℕ) [NeZero n] : NonUnitalCommRing (Fin n)

Equations

• One or more equations did not get rendered due to their size.

instance Fin.instCommMonoid (n : ℕ) [NeZero n] : CommMonoid (Fin n)

Equations

• One or more equations did not get rendered due to their size.

instance Fin.instHasDistribNeg (n : ℕ) : HasDistribNeg (Fin n)

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

Equations

• Fin.instHasDistribNeg n = { toInvolutiveNeg := Fin.instInvolutiveNeg n, neg_mul := ⋯, mul_neg := ⋯ }

def Fin.instCommRing (n : ℕ) [NeZero n] : CommRing (Fin n)

Commutative ring structure on Fin n.

This is not a global instance, but can introduced locally using open Fin.CommRing in ....

This is not an instance because the binop% elaborator assumes that htere are no non-trivial coercion loops, but this instance would introduce a coercion from Nat to Fin n and back. Non-trivial loops lead to undesirable and counterintuitive elaboration behavior.

For example, for x : Fin k and n : Nat, it causes x < n to be elaborated as x < ↑n rather than ↑x < n, silently introducing wraparound arithmetic.

Equations

• One or more equations did not get rendered due to their size.

instance Fin.instNeZeroHAddNatOfNat_mathlib (n : ℕ) [NeZero n] : NeZero 1

def ZMod : ℕ → Type

The integers modulo n : ℕ.

Equations

• ZMod 0 = ℤ
• ZMod n.succ = Fin (n + 1)

instance ZMod.decidableEq (n : ℕ) : DecidableEq (ZMod n)

Equations

• ZMod.decidableEq 0 = inferInstanceAs (DecidableEq ℤ)
• ZMod.decidableEq n.succ = inferInstanceAs (DecidableEq (Fin (n + 1)))

instance ZMod.repr (n : ℕ) : Repr (ZMod n)

Equations

• ZMod.repr 0 = id inferInstance
• ZMod.repr n.succ = id inferInstance

instance ZMod.instUnique : Unique (ZMod 1)

Equations

• ZMod.instUnique = Fin.instUnique

instance ZMod.fintype (n : ℕ) [NeZero n] : Fintype (ZMod n)

Equations

• ZMod.fintype 0 = ⋯.elim
• ZMod.fintype n.succ = Fin.fintype (n + 1)

instance ZMod.infinite : Infinite (ZMod 0)

@[simp]

theorem ZMod.card (n : ℕ) [Fintype (ZMod n)] : Fintype.card (ZMod n) = n

instance ZMod.commRing (n : ℕ) : CommRing (ZMod n)

Equations

• One or more equations did not get rendered due to their size.

instance ZMod.inhabited (n : ℕ) : Inhabited (ZMod n)

Equations

• ZMod.inhabited n = { default := 0 }