Documentation

Mathlib.Data.ZMod.QuotientRing

ZMod n and quotient groups / rings #

This file relates ZMod n to the quotient ring ℤ ⧸ Ideal.span {(n : ℤ)}.

Main definitions #

Tags #

zmod, quotient ring, ideal quotient

source
def Int.quotientSpanNatEquivZMod (n : ℕ) :
ℤ ⧸ Ideal.span {↑n} ≃+* ZMod n

ℤ modulo the ideal generated by n : ℕ is ZMod n.

Equations
Instances For
    source
    def Int.quotientSpanEquivZMod (a : ℤ) :
    ℤ ⧸ Ideal.span {a} ≃+* ZMod a.natAbs

    ℤ modulo the ideal generated by a : ℤ is ZMod a.natAbs.

    Equations
    Instances For
      source
      @[simp]
      theorem Int.quotientSpanNatEquivZMod_comp_Quotient_mk (n : ℕ) :
      (↑(quotientSpanNatEquivZMod n)).comp (Ideal.Quotient.mk (Ideal.span {↑n})) = castRingHom (ZMod n)
      source
      @[simp]
      theorem Int.quotientSpanNatEquivZMod_comp_castRingHom (n : ℕ) :
      (↑(quotientSpanNatEquivZMod n).symm).comp (castRingHom (ZMod n)) = Ideal.Quotient.mk (Ideal.span {↑n})
      source
      @[simp]
      theorem Int.quotientSpanEquivZMod_comp_Quotient_mk (n : ℤ) :
      (↑n.quotientSpanEquivZMod).comp (Ideal.Quotient.mk (Ideal.span {n})) = castRingHom (ZMod n.natAbs)
      source
      @[simp]
      theorem Int.quotientSpanEquivZMod_comp_castRingHom (n : ℤ) :
      (↑n.quotientSpanEquivZMod.symm).comp (castRingHom (ZMod n.natAbs)) = Ideal.Quotient.mk (Ideal.span {n})
      source
      instance Int.instFiniteQuotientIdealSpanSingletonSetOfNeZero {n : ℤ} [NeZero n] :
      Finite (ℤ ⧸ Ideal.span {n})
      source
      noncomputable def ZMod.prodEquivPi {ι : Type u_2} [Fintype ι] (a : ι → ℕ) (coprime : Pairwise (Function.onFun Nat.Coprime a)) :
      ZMod (∏ i : ι, a i) ≃+* ((i : ι) → ZMod (a i))

      The Chinese remainder theorem, elementary version for ZMod. See also Mathlib/Data/ZMod/Basic.lean for versions involving only two numbers.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem ZMod.prodEquivPi_apply {ι : Type u_2} [Fintype ι] (a : ι → ℕ) (coprime : Pairwise (Function.onFun Nat.Coprime a)) (b : ZMod (∏ i : ι, a i)) (i : ι) :
        (prodEquivPi a coprime) b i = (castHom ⋯ (ZMod (a i))) b
        source
        noncomputable def ZMod.equivPi (n : ℕ) (hn : n ≠ 0) :
        ZMod n ≃+* ((p : ↥n.primeFactors) → ZMod (↑p ^ n.factorization ↑p))

        The Chinese remainder theorem, version for ZMod n.

        Equations
        Instances For