Commit 2022-04-12 08:46 72e1a9ee

feat(ring_theory/valuation/valuation_ring): Valuation rings and their associated valuation. (#12719) This PR defines a class valuation_ring, stating that an integral domain is a valuation ring. We also show that valuation rings induce valuations on their fraction fields, that valuation rings are local, and that their lattice of ideals is totally ordered.