feat(algebra/archimedean): add fractional parts of floor_rings

[kbuzzard]

TO CONTRIBUTORS:

Make sure you have:

• reviewed and applied the coding style: coding, naming
• for tactics:
  • added or adapted documentation in tactics.md
  • write an example of use of the new feature in tactics.lean
• make sure definitions and lemmas are put in the right files
• make sure definitions and lemmas are not redundant

If this PR is related to a discussion on Zulip, please include a link in the discussion.

For reviewers: code review check list

---

This is a theory of fractional parts of reals and more general floor_rings, i.e. fract r := r - floor r.

Note that I've added another import, abel, to algebra/archimedean.lean; linarith imports ring but I can't use ring because a floor_ring is not necessarily commutative. Without this import I would have to directly prove something of the form a+(b+c)-(b-a)=c, that sort of thing, which I could do but didn't.

[This is the same as #703, where a little rebasing experiment of mine went wrong]