Multiplicative_Ordering_on_Integers

Proved

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

integer-multiplicationorderings-on-integersproofwiki

Let $x, y, z \in \Z$ such that $z > 0$ . Then $x < y \iff z x < z y$ $x \le y \iff z x \le z y$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Multiplicative_Ordering_on_Integers (x y z : ℤ) (hz : 0 < z) : x < y ↔ z * x < z * y := by sorry

Source