# Zulip Chat Archive

## Stream: general

### Topic: What is this Real-like number system

#### Locria Cyber (Aug 16 2022 at 12:06):

```
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 (Aug 16 2022 at 12:08):

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

#### Locria Cyber (Aug 16 2022 at 12:09):

Someone must have given this number system a name before.

#### Yaël Dillies (Aug 16 2022 at 12:09):

#### Yaël Dillies (Aug 16 2022 at 12:10):

Actually it's more like `field`

+ `linear_order`

+ `0 < 1`

, because you're not requiring any monotonicity on `+`

and `*`

.

#### Jason Rute (Aug 16 2022 at 12:29):

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 (Aug 16 2022 at 12:35):

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

#### Jason Rute (Aug 16 2022 at 12:51):

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.

Last updated: Dec 20 2023 at 11:08 UTC