Smaug123 / agdaproofs

Mathematical proofs in Agda
MIT License
4 stars 1 forks source link

Comparison on the reals #55

Closed Smaug123 closed 5 years ago

Smaug123 commented 5 years ago

Still remaining: multiplication. (This was blocked on the comparison work, because to show that multiplication is well-defined requires bounding a real number by a rational.)