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