Integer_Divisor_is_Equivalent_to_Subset_of_Ideal

Proved

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

divisibilityidealsintegersproofwikiring-theory

Let $\Z$ be the set of all integers. Let $\Z_{>0}$ be the set of strictly positive integers. Let $m \in \Z_{>0}$ and let $n \in \Z$ . Let $\ideal m$ be the principal ideal of $\Z$ generated by $m$ . Then $m \divides n \iff \ideal n \subseteq \ideal m$

Preamble

import Mathlib.Analysis.Complex.Basic
import Mathlib.RingTheory.PrincipalIdealDomain

Formal statement

theorem Integer_Divisor_is_Equivalent_to_Subset_of_Ideal (m n : ℤ) (hm : 0 < m) (hn : 0 < n) : m ∣ n ↔ Ideal.span ({n} : Set ℤ) ≤ Ideal.span ({m} : Set ℤ) := by sorry

Source

https://proofwiki.org/wiki/Integer_Divisor_is_Equivalent_to_Subset_of_Ideal

View graph