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

source
@[simp]
theorem Fin.val_intCast {n : ℕ} [NeZero n] (x : ℤ) :
↑↑x = (x % ↑n).toNat
source
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 := ⋯ }

source
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 := ⋯ }

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

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

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

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

source
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 := ⋯ }

source
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 there 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.

Instances For

source
instance Fin.instNeZeroHAddNatOfNat_mathlib_1 (n : ℕ) [NeZero n] :
NeZero 1
source
def ZMod :
ℕ → Type

The integers modulo `n : ℕ`.

Equations

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

Instances For

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

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

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

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

source
instance ZMod.instUnique :
Unique (ZMod 1)
Equations

- ZMod.instUnique = Fin.instUnique

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

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

source
instance ZMod.infinite :
Infinite (ZMod 0)
source
@[simp]
theorem ZMod.card (n : ℕ) [Fintype (ZMod n)] :
Fintype.card (ZMod n) = n
source
instance ZMod.commRing (n : ℕ) :
CommRing (ZMod n)
Equations

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

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

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