Commit 2022-06-08 18:51 9c4a3d1b

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.