Subgroup_of_Integers_is_Ideal

Proved

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

idealsintegersproofwikiring-theorysubgroups

Let $\struct {\Z, +}$ be the additive group of integers. Every subgroup of $\struct {\Z, +}$ is an ideal of the ring $\struct {\Z, +, \times}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Subgroup_of_Integers_is_Ideal (H : AddSubgroup ℤ) : ∀ (r : ℤ) (h : ℤ), h ∈ H → r * h ∈ H := by sorry

Source