Commit 2022-08-10 15:00 e63df397

feat(ring_theory/valuation/valuation_subring): define principal unit group of valuation subring and provide basic API (#14742) This PR defines the principal unit group of a valuation subring as a subgroup of the units of the field. We show two valuation subrings are equal iff their principal unit groups are the same, and we show that the map on valuation subrings to their principal unit groups is an order embedding.