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 = CommSemigroup.mk ⋯

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

Commutative ring structure on Fin n.

Equations

• Fin.instDistrib n = Distrib.mk ⋯ ⋯

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

Commutative ring structure on Fin n.

Equations

• Fin.instCommRing n = CommRing.mk ⋯

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 = HasDistribNeg.mk ⋯ ⋯

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.uniqueFinOne

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)

Equations

• ZMod.infinite = Int.infinite

@[simp]

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

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

Equations

• ZMod.commRing n = CommRing.mk ⋯

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

Equations

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