## Stream: maths

### Topic: ring requires linear order

#### Chris Hughes (Dec 02 2018 at 01:42):

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 (Dec 02 2018 at 09:46):

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

Last updated: May 19 2021 at 02:10 UTC