mathlib3

b1a1ece3 - feat(ring_theory/valuation/valuation_subring): The order structure on valuation subrings of a field (#13429)

feat(ring_theory/valuation/valuation_subring): The order structure on valuation subrings of a field (#13429) This PR shows that for a valuation subring `R` of a field `K`, the coarsenings of `R` are in (anti)ordered bijections with the prime ideals of `R`. As a corollary, the collection of such coarsenings is totally ordered. Co-authored-by: Junyan Xu <junyanxumath@gmail.com>