Mathlib.Data.ZMod.Defs

Module docstring

{"# 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. "}

Fin.instCommSemigroup instance

(n : ℕ) : CommSemigroup (Fin n)

Full source

/-- Multiplicative commutative semigroup structure on `Fin n`. -/
instance instCommSemigroup (n : ℕ) : CommSemigroup (Fin n) :=
  { inferInstanceAs (Mul (Fin n)) with
    mul_assoc := fun ⟨a, _⟩ ⟨b, _⟩ ⟨c, _⟩ =>
      Fin.eq_of_val_eq <|
        calc
          a * b % n * c ≡ a * b * c [MOD n] := (Nat.mod_modEq _ _).mul_right _
          _ ≡ a * (b * c) [MOD n]calc
          a * b % n * c ≡ a * b * c [MOD n] := (Nat.mod_modEq _ _).mul_right _
          _ ≡ a * (b * c) [MOD n] := by rw [mul_assoc]
          _ ≡ a * (b * c % n) [MOD n] := (Nat.mod_modEq _ _).symm.mul_left _
    mul_comm := Fin.mul_comm }

Commutative Semigroup Structure on Finite Types

Informal description

For any natural number $n$, the finite type $\text{Fin}\ n$ has a canonical structure of a commutative semigroup with multiplication.

Fin.instDistrib instance

(n : ℕ) : Distrib (Fin n)

Full source

/-- Commutative ring structure on `Fin n`. -/
instance instDistrib (n : ℕ) : Distrib (Fin n) :=
  { Fin.addCommSemigroup n, Fin.instCommSemigroup n with
    left_distrib := left_distrib_aux n
    right_distrib := fun a b c => by
      rw [mul_comm, left_distrib_aux, mul_comm _ b, mul_comm] }

Distributivity of Multiplication over Addition in $\mathrm{Fin}\,n$

Informal description

For any natural number $n$, the finite type $\mathrm{Fin}\,n$ has a distributive structure, meaning that multiplication distributes over addition: $a \cdot (b + c) = a \cdot b + a \cdot c$ and $(a + b) \cdot c = a \cdot c + b \cdot c$ for all $a, b, c \in \mathrm{Fin}\,n$.

Fin.instCommRing instance

(n : ℕ) [NeZero n] : CommRing (Fin n)

Full source

/-- Commutative ring structure on `Fin n`. -/
instance instCommRing (n : ℕ) [NeZero n] : CommRing (Fin n) :=
  { Fin.instAddMonoidWithOne n, Fin.addCommGroup n, Fin.instCommSemigroup n, Fin.instDistrib n with
    one_mul := Fin.one_mul'
    mul_one := Fin.mul_one',
    zero_mul := Fin.zero_mul'
    mul_zero := Fin.mul_zero' }

Commutative Ring Structure on $\mathrm{Fin}(n)$

Informal description

For any nonzero natural number $n$, the finite type $\mathrm{Fin}(n)$ (the set $\{0, 1, \dots, n-1\}$) forms a commutative ring under addition and multiplication modulo $n$.

Fin.instHasDistribNeg instance

(n : ℕ) : HasDistribNeg (Fin n)

Full source

/-- Note this is more general than `Fin.instCommRing` as it applies (vacuously) to `Fin 0` too. -/
instance instHasDistribNeg (n : ℕ) : HasDistribNeg (Fin n) :=
  { toInvolutiveNeg := Fin.instInvolutiveNeg n
    mul_neg := Nat.casesOn n finZeroElim fun _i => mul_neg
    neg_mul := Nat.casesOn n finZeroElim fun _i => neg_mul }

Distributivity of Negation over Multiplication in $\mathrm{Fin}(n)$

Informal description

For any natural number $n$, the negation operation on $\mathrm{Fin}(n)$ distributes over multiplication, meaning that $- (a * b) = (-a) * b = a * (-b)$ for all $a, b \in \mathrm{Fin}(n)$.

ZMod definition

: ℕ → Type

Full source

/-- The integers modulo `n : ℕ`. -/
def ZMod : ℕ → Type
  | 0 => ℤ
  | n + 1 => Fin (n + 1)

Integers modulo $ n $ ($\mathbb{Z}/n\mathbb{Z}$)

Informal description

The integers modulo $ n $, denoted $\mathbb{Z}/n\mathbb{Z}$, is defined as: - The integers $\mathbb{Z}$ when $ n = 0 $ - The finite type with $ n $ elements (represented as $\text{Fin } n$) when $ n \geq 1 $

ZMod.decidableEq instance

: ∀ n : ℕ, DecidableEq (ZMod n)

Full source

instance ZMod.decidableEq : ∀ n : ℕ, DecidableEq (ZMod n)
  | 0 => inferInstanceAs (DecidableEq ℤ)
  | n + 1 => inferInstanceAs (DecidableEq (Fin (n + 1)))

Decidability of Equality in $\mathbb{Z}/n\mathbb{Z}$

Informal description

For every natural number $n$, the integers modulo $n$ ($\mathbb{Z}/n\mathbb{Z}$) have decidable equality.

ZMod.repr instance

: ∀ n : ℕ, Repr (ZMod n)

Full source

instance ZMod.repr : ∀ n : ℕ, Repr (ZMod n)
  | 0 => by dsimp [ZMod]; infer_instance
  | n + 1 => by dsimp [ZMod]; infer_instance

String Representation of Integers Modulo $n$

Informal description

For every natural number $n$, the integers modulo $n$ ($\mathbb{Z}/n\mathbb{Z}$) have a canonical string representation.

ZMod.instUnique instance

: Unique (ZMod 1)

Full source

instance instUnique : Unique (ZMod 1) := Fin.instUnique

Uniqueness of $\mathbb{Z}/1\mathbb{Z}$

Informal description

The integers modulo 1, $\mathbb{Z}/1\mathbb{Z}$, has exactly one element.

ZMod.fintype instance

: ∀ (n : ℕ) [NeZero n], Fintype (ZMod n)

Full source

instance fintype : ∀ (n : ℕ) [NeZero n], Fintype (ZMod n)
  | 0, h => (h.ne _ rfl).elim
  | n + 1, _ => Fin.fintype (n + 1)

Finiteness of Integers Modulo $n$ for $n \neq 0$

Informal description

For any nonzero natural number $n$, the integers modulo $n$ ($\mathbb{Z}/n\mathbb{Z}$) form a finite type with exactly $n$ elements.

ZMod.infinite instance

: Infinite (ZMod 0)

Full source

instance infinite : Infinite (ZMod 0) :=
  Int.infinite

Infinite Structure of $\mathbb{Z}/0\mathbb{Z}$

Informal description

The integers modulo 0, $\mathbb{Z}/0\mathbb{Z}$, is an infinite type.

ZMod.card theorem

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

Full source

@[simp]
theorem card (n : ℕ) [Fintype (ZMod n)] : Fintype.card (ZMod n) = n := by
  cases n with
  | zero => exact (not_finite (ZMod 0)).elim
  | succ n => convert Fintype.card_fin (n + 1) using 2

Cardinality of $\mathbb{Z}/n\mathbb{Z}$ is $n$

Informal description

For any natural number $n$, if $\mathbb{Z}/n\mathbb{Z}$ is a finite type, then its cardinality is equal to $n$, i.e., $|\mathbb{Z}/n\mathbb{Z}| = n$.

ZMod.commRing instance

(n : ℕ) : CommRing (ZMod n)

Full source

instance commRing (n : ℕ) : CommRing (ZMod n) where
  add := Nat.casesOn n (@Add.add Int _) fun n => @Add.add (Fin n.succ) _
  add_assoc := Nat.casesOn n (@add_assoc Int _) fun n => @add_assoc (Fin n.succ) _
  zero := Nat.casesOn n (0 : Int) fun n => (0 : Fin n.succ)
  zero_add := Nat.casesOn n (@zero_add Int _) fun n => @zero_add (Fin n.succ) _
  add_zero := Nat.casesOn n (@add_zero Int _) fun n => @add_zero (Fin n.succ) _
  neg := Nat.casesOn n (@Neg.neg Int _) fun n => @Neg.neg (Fin n.succ) _
  sub := Nat.casesOn n (@Sub.sub Int _) fun n => @Sub.sub (Fin n.succ) _
  sub_eq_add_neg := Nat.casesOn n (@sub_eq_add_neg Int _) fun n => @sub_eq_add_neg (Fin n.succ) _
  zsmul := Nat.casesOn n
    (inferInstanceAs (CommRing ℤ)).zsmul fun n => (inferInstanceAs (CommRing (Fin n.succ))).zsmul
  zsmul_zero' := Nat.casesOn n
    (inferInstanceAs (CommRing ℤ)).zsmul_zero'
    fun n => (inferInstanceAs (CommRing (Fin n.succ))).zsmul_zero'
  zsmul_succ' := Nat.casesOn n
    (inferInstanceAs (CommRing ℤ)).zsmul_succ'
    fun n => (inferInstanceAs (CommRing (Fin n.succ))).zsmul_succ'
  zsmul_neg' := Nat.casesOn n
    (inferInstanceAs (CommRing ℤ)).zsmul_neg'
    fun n => (inferInstanceAs (CommRing (Fin n.succ))).zsmul_neg'
  nsmul := Nat.casesOn n
    (inferInstanceAs (CommRing ℤ)).nsmul fun n => (inferInstanceAs (CommRing (Fin n.succ))).nsmul
  nsmul_zero := Nat.casesOn n
    (inferInstanceAs (CommRing ℤ)).nsmul_zero
    fun n => (inferInstanceAs (CommRing (Fin n.succ))).nsmul_zero
  nsmul_succ := Nat.casesOn n
    (inferInstanceAs (CommRing ℤ)).nsmul_succ
    fun n => (inferInstanceAs (CommRing (Fin n.succ))).nsmul_succ
  neg_add_cancel := Nat.casesOn n (@neg_add_cancel Int _) fun n => @neg_add_cancel (Fin n.succ) _
  add_comm := Nat.casesOn n (@add_comm Int _) fun n => @add_comm (Fin n.succ) _
  mul := Nat.casesOn n (@Mul.mul Int _) fun n => @Mul.mul (Fin n.succ) _
  mul_assoc := Nat.casesOn n (@mul_assoc Int _) fun n => @mul_assoc (Fin n.succ) _
  one := Nat.casesOn n (1 : Int) fun n => (1 : Fin n.succ)
  one_mul := Nat.casesOn n (@one_mul Int _) fun n => @one_mul (Fin n.succ) _
  mul_one := Nat.casesOn n (@mul_one Int _) fun n => @mul_one (Fin n.succ) _
  natCast := Nat.casesOn n ((↑) : ℕ → ℤ) fun n => ((↑) : ℕ → Fin n.succ)
  natCast_zero := Nat.casesOn n (@Nat.cast_zero Int _) fun n => @Nat.cast_zero (Fin n.succ) _
  natCast_succ := Nat.casesOn n (@Nat.cast_succ Int _) fun n => @Nat.cast_succ (Fin n.succ) _
  intCast := Nat.casesOn n ((↑) : ℤ → ℤ) fun n => ((↑) : ℤ → Fin n.succ)
  intCast_ofNat := Nat.casesOn n (@Int.cast_natCast Int _) fun n => @Int.cast_natCast (Fin n.succ) _
  intCast_negSucc :=
    Nat.casesOn n (@Int.cast_negSucc Int _) fun n => @Int.cast_negSucc (Fin n.succ) _
  left_distrib := Nat.casesOn n (@left_distrib Int _ _ _) fun n => @left_distrib (Fin n.succ) _ _ _
  right_distrib :=
    Nat.casesOn n (@right_distrib Int _ _ _) fun n => @right_distrib (Fin n.succ) _ _ _
  mul_comm := Nat.casesOn n (@mul_comm Int _) fun n => @mul_comm (Fin n.succ) _
  zero_mul := Nat.casesOn n (@zero_mul Int _) fun n => @zero_mul (Fin n.succ) _
  mul_zero := Nat.casesOn n (@mul_zero Int _) fun n => @mul_zero (Fin n.succ) _
  npow := Nat.casesOn n
    (inferInstanceAs (CommRing ℤ)).npow fun n => (inferInstanceAs (CommRing (Fin n.succ))).npow
  npow_zero := Nat.casesOn n
    (inferInstanceAs (CommRing ℤ)).npow_zero
    fun n => (inferInstanceAs (CommRing (Fin n.succ))).npow_zero
  npow_succ := Nat.casesOn n
    (inferInstanceAs (CommRing ℤ)).npow_succ
    fun n => (inferInstanceAs (CommRing (Fin n.succ))).npow_succ

Commutative Ring Structure on $\mathbb{Z}/n\mathbb{Z}$

Informal description

For any natural number $n$, the integers modulo $n$ ($\mathbb{Z}/n\mathbb{Z}$) form a commutative ring.

ZMod.inhabited instance

(n : ℕ) : Inhabited (ZMod n)

Full source

instance inhabited (n : ℕ) : Inhabited (ZMod n) :=
  ⟨0⟩

Inhabitedness of Integers Modulo $n$

Informal description

For any natural number $n$, the integers modulo $n$ ($\mathbb{Z}/n\mathbb{Z}$) is an inhabited type, meaning it has at least one element.