Divisor_Relation_on_Positive_Integers_is_Partial_Ordering
Proveddivisorsintegersorder-theoryproofwiki
The divisor relation is a partial ordering on the positive integers.
Preamble
import Mathlib.Data.Int.GCD import Mathlib.Order.RelClasses
Formal statement
theorem Divisor_Relation_on_Positive_Integers_is_Partial_Ordering : IsPartialOrder {n : ℤ | 0 < n} (fun a b => (a : ℤ) ∣ (b : ℤ)) := by sorrySource