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.

Equations

• Int.quotientSpanNatEquivZMod n = (Ideal.quotEquivOfEq ⋯).symm.trans (RingHom.quotientKerEquivOfRightInverse ⋯)

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

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

Equations

• a.quotientSpanEquivZMod = (Ideal.quotEquivOfEq ⋯).symm.trans (Int.quotientSpanNatEquivZMod 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})

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.

Equations

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