Finish the construction of the structure of a field on reals

JetBrains / arend-lib

Apache License 2.0

79 stars 23 forks source link

Closed valis closed 3 months ago

valis commented 1 year ago

There are several goals left in Arith.Real:

[x] The locatedness property for the product of two reals.
[x] The locatedness property for the inverse of a positive real.
[x] Various properties of the product, including associativity, commutativity, and distributivity.