mathlib3

8bc2354c - feat(ring_theory/valuation/valuation_subring): define maximal ideal of valuation subring and provide basic API (#14656)

feat(ring_theory/valuation/valuation_subring): define maximal ideal of valuation subring and provide basic API (#14656) This PR defines the unique maximal ideal of a valuation subring as a subsemigroup of the field. We prove a few equivalent conditions for two valuations to be equivalent, and we use this to show two valuation subrings are equivalent iff they have the same maximal ideal. Co-authored-by: Vierkantor <vierkantor@vierkantor.com> Co-authored-by: jackmckoen <104791831+jackmckoen@users.noreply.github.com>