feat(ring_theory/valuation/valuation_subring): Supremum of families of valuation rings.

[adamtopaz]

Adds two definitions:

• The supremum of a directed family of valuation rings, as a valuation ring.
• The supremum of a family of valuation rings which are bounded below by some fixed valuation ring, as a valuation ring.

In both cases, the carrier set is defeq to the union of the family.

---

[bors[bot]]

:v: adamtopaz can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.