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
0 < 1, because you're not requiring any monotonicity on
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: Aug 03 2023 at 10:10 UTC