Zulip Chat Archive

Stream: maths

Topic: ring requires linear order


view this post on Zulip 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

view this post on Zulip 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