ring requires linear order

Stream: maths

[Chris Hughes]

Is this a non-trivial upgrade? The support for division in ring only works on ordered fields.

import tactic.ring data.complex.basic

example (x : ℝ) : x / 3 + x / 2 = 5 * x / 6 := by ring --works

example (x : ℂ) : x / 3 + x / 2 = 5 * x / 6 := by ring --fails

[Kevin Buzzard]

I vaguely remember a conversation at one point where I asked Mario why something had to be ordered, and at the time it was because actually the thing had to be characteristic zero and there was no characteristic zero predicate at the time, but ordered implied it