Quotient_Group_of_Integers_by_Multiples

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

group-theoryintegersmodular-arithmeticproofwikiquotient-groups

Let $\struct {\Z, +}$ be the additive group of integers. Let $\struct {m \Z, +}$ be the additive group of integer multiples of $m$ . Let $\struct {\Z_m, +_m}$ be the additive group of integers modulo $m$ . Then the quotient group of $\struct {\Z, +}$ by $\struct {m \Z, +}$ is $\struct {\Z_m, +_m}$ . Thus $\index \Z {m \Z} = m$

Preamble

import Mathlib.Analysis.Complex.Basic
import Mathlib.Data.ZMod.Basic

Formal statement

theorem Quotient_Group_of_Integers_by_Multiples (m : ℕ) [NeZero m] : Nonempty ((ℤ ⧸ AddSubgroup.closure ({(m : ℤ)} : Set ℤ)) ≃+ ZMod m) := by sorry

Source

https://proofwiki.org/wiki/Quotient_Group_of_Integers_by_Multiples

View graph