Congruences_on_Rational_Numbers

Proved

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

congruence-relationsproofwikirational-numbers

There are only two congruence relations on the field of rational numbers $\left({\Q, +, \times}\right)$ $(1): \quad$ The diagonal relation $\Delta_\Q$ $(2): \quad$ The trivial relation $\Q \times \Q$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Congruences_on_Rational_Numbers (r : Setoid ℚ) (hmul : ∀ a b c d : ℚ, r.r a b → r.r c d → r.r (a * c) (b * d)) (hadd : ∀ a b c d : ℚ, r.r a b → r.r c d → r.r (a + c) (b + d)) : (∀ a b : ℚ, r.r a b) ∨ (∀ a b : ℚ, r.r a b → a = b) := by sorry

Source

https://proofwiki.org/wiki/Congruences_on_Rational_Numbers

View graph