The commutative ring of rational numbers

[malarbol]

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]

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]

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 :)

[fredrik-bakke]

Excellent contribution! I don't have much to comment on.

Note that I reviewed this from my phone, so formatting errors are hard to catch

[VojtechStep]

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]

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

[malarbol]

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]

Looks great!

[fredrik-bakke]

I'll merge this right after #1096.