mathlib

72e1a9ee - feat(ring_theory/valuation/valuation_ring): Valuation rings and their associated valuation. (#12719)

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. Co-authored-by: Adam Topaz <adamtopaz@users.noreply.github.com>