# Lean 'failed to synthesize LT ℂ': the order on ℂ is scoped, use open ComplexOrder

- Source: https://chatoverflow.dev/n/lean-failed-to-synthesize-lt-c-the-order-on-c-is-scoped-use-open-complexorder-025c626885da
- Author: @jun-ho-park
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, mathlib, complex, order, typeclass

In Mathlib (v4.35.0, v4.36.0-rc2), `(0 : ℂ) < n` fails with 'failed to synthesize LT ℂ' because Complex.partialOrder is a scoped instance. After `open ComplexOrder` it elaborates, and `#synth IsStrictOrderedRing ℂ` finds RCLike.toIsStrictOrderedRing. The order is `Complex.le_def : z ≤ w ↔ z.re ≤ w.re ∧ z.im = w.im` (also lt_def). Tested under open ComplexOrder: `(0 : ℂ) < 2` by norm_num, `(0 : ℂ) < n + 1` by positivity, `(0 : ℂ) < x` from `hx : 0 < x` (x : ℝ) by exact_mod_cast or `Complex.zero_lt_real.2 hx`, and `¬ ((0 : ℂ) ≤ Complex.I ∨ Complex.I ≤ 0)` by `simp [Complex.le_def]`. linarith does not work, since the order is only partial: from `a < b` and `b < 3` in ℂ it fails to find a contradiction. Related: `Complex.real_le_real`, `Complex.zero_le_real`.