What is this Real-like number system

Stream: general

[Locria Cyber]

axiom R : Type

class Inv (α : Type u) where
  inv : α → α

prefix:100 "/"    => Inv.inv

namespace R

axiom R0 : R
axiom R1 : R

noncomputable
instance : OfNat R 0 where
  ofNat := R0

noncomputable
instance : OfNat R 1 where
  ofNat := R1


axiom opp : R -> R
axiom plus : R -> R -> R

noncomputable
instance : Neg R where
  neg := opp

noncomputable
instance : Add R where
  add := plus


axiom inv : R -> R
axiom mult : R -> R -> R

noncomputable
instance : Inv R where
  inv := inv

noncomputable
instance : Mul R where
  mul := mult

axiom plus_opp_r (r: R) : r + -r = 0
axiom mult_inv_r (r: R) : r * /r = 1

axiom plus_comm (a: R) (b: R) : a + b = b + a
axiom mult_comm (a: R) (b: R) : a * b = b * a


axiom lt : R -> R -> Prop

noncomputable
instance : LT R where
  lt := lt

axiom lt_is_not_eq (a: R) (b: R) : ¬ (lt a b ∧ a = b)
axiom lt_trans (a: R) (b: R) (c: R) : a < b ∧ b < c -> a < c
axiom r0_lt_1 : lt 0 1

end R

[Locria Cyber]

This is not quite Real numbers, since 0 has properly defined inverse

[Locria Cyber]

Someone must have given this number system a name before.

[Yaël Dillies]

docs#linear_ordered_field?

[Yaël Dillies]

Actually it's more like field + linear_order + 0 < 1, because you're not requiring any monotonicity on + and *.

[Jason Rute]

If you add associativity of addition and multiplication and distributivity (edit: and that 0 and 1 are identities), then you would have a field where 0 has an inverse but 0 != 1. That would be a contradiction. But since you have no rules on how plus and times play together, I guess you could just have two groups on the same set that have little to do with each other. For example your + could be the usual addition on the reals. Then x * y could be shifted plus, namely (x - 1) + (y -1) + 1 or something like that.

[Jason Rute]

If you haven’t already, I think you would enjoy learning abstract algebra.

[Jason Rute]

Another trivial solution: x + y is always 0 (and -x could be anything including just x) and x * y is always 1. This works because you don’t even assume 0 and 1 are identities.