No linear order on Complex (Lean4)

Stream: new members

[Jiatong Yang]

import Mathlib

open Complex

theorem thm [LinearOrderedField ℂ] : False := by
  have h : 0 ≤ I ^ 2 := sq_nonneg I

I want to prove that there is no linear order on ℂ. But the code above does not compile due to some typeclass issue. I need help.

[Kenny Lau]

@Jiatong Yang if you hover over the red underline, it tells you the correct thing to put there

[Yiming Fu]

(deleted)

[Yiming Fu]

That works:

import Mathlib

open Complex

theorem thm [LinearOrder ℂ] [IsStrictOrderedRing ℂ] : False := by
  have h : 0 ≤ I ^ 2 := sq_nonneg I
  sorry