ZMod n and quotient groups / rings

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

Main definitions

• ZMod.quotient_span_nat_equiv_zmod and ZMod.quotientSpanEquivZMod : ZMod n is the ring quotient of ℤ by n ℤ : Ideal.span {n} (where n : ℕ and n : ℤ respectively)

Tags

zmod, quotient ring, ideal quotient

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

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

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

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

@[simp]

theorem Int.quotientSpanNatEquivZMod_comp_Quotient_mk (n : ℕ) : (↑(quotientSpanNatEquivZMod n)).comp (Ideal.Quotient.mk (Ideal.span {↑n})) = castRingHom (ZMod n)

@[simp]

theorem Int.quotientSpanNatEquivZMod_comp_castRingHom (n : ℕ) : (↑(quotientSpanNatEquivZMod n).symm).comp (castRingHom (ZMod n)) = Ideal.Quotient.mk (Ideal.span {↑n})

@[simp]

theorem Int.quotientSpanEquivZMod_comp_Quotient_mk (n : ℤ) : (↑n.quotientSpanEquivZMod).comp (Ideal.Quotient.mk (Ideal.span {n})) = castRingHom (ZMod n.natAbs)

@[simp]

theorem Int.quotientSpanEquivZMod_comp_castRingHom (n : ℤ) : (↑n.quotientSpanEquivZMod.symm).comp (castRingHom (ZMod n.natAbs)) = Ideal.Quotient.mk (Ideal.span {n})

instance Int.instFiniteQuotientIdealSpanSingletonSetOfNeZero {n : ℤ} [NeZero n] : Finite (ℤ ⧸ Ideal.span {n})

noncomputable def ZMod.prodEquivPi {ι : Type u_3} [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.

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.