mathlib3

9c4a3d1b - feat(ring_theory/valuation/valuation_subring): define unit group of valuation subring and provide basic API (#14540)

feat(ring_theory/valuation/valuation_subring): define unit group of valuation subring and provide basic API (#14540) This PR defines the unit group of a valuation subring as a multiplicative subgroup of the units of the field. We show two valuation subrings are equivalent iff they have the same unit group. We show the map sending a valuation to its unit group is an order embedding. Co-authored-by: Adam Topaz <github@adamtopaz.com> Co-authored-by: jackmckoen <104791831+jackmckoen@users.noreply.github.com>