Integers_form_Totally_Ordered_Ring

Proved

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

integersproofwikitotally-ordered-rings

The structure $\struct {\Z, +, \times, \le}$ is a totally ordered ring.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Integers_form_Totally_Ordered_Ring (a b c : ℤ) (h : a ≤ b) (hc : 0 ≤ c) : a * c ≤ b * c := by sorry

Source