The commutative ring of rational numbers

UniMath / agda-unimath

The agda-unimath library

https://unimath.github.io/agda-unimath/

MIT License

219 stars 70 forks source link

The commutative ring of rational numbers #1107

Closed malarbol closed 5 months ago

malarbol commented 5 months ago

This pull request introduces the commutative ring structure on the rational numbers.

We introduce:

left distributivity of multiplication over the addition of integer fractions;
(left|right) distributivity of multiplication over the addition of rational numbers (the last missing law for the ring structure);
(left|right) distributivity of multiplication over the difference of rational numbers;
a few laws about multiplication by zero in the rational numbers.

malarbol commented 5 months ago

I'm back for more elementary-number-theory. Hopefully this new PR will be less work than the last one. It's quite small and the changes are pretty straightforward.

fredrik-bakke commented 5 months ago

Do you know why I usually write (left|right) by the way? It's because that's how you write the regex to match either word :)

VojtechStep commented 5 months ago

There's a malformed link in elementary-number-theory.addition-rational-numbers to group-of-rational-numbers that we didn't catch in the last PR - @malarbol would you mind fixing it in this PR?

fredrik-bakke commented 5 months ago

Oh, did you implement all the requested changes, @malarbol? Is this ready to merge?

malarbol commented 5 months ago

Oh, did you implement all the requested changes, @malarbol? Is this ready to merge?

I think I did (have a last check maybe?) and that it's ready to merge.

fredrik-bakke commented 5 months ago

I'll merge this right after #1096.