mathlib3

c241a033 - docs(ring_theory/valuation/valuation_subring): clarify value group docstring (#16272)

docs(ring_theory/valuation/valuation_subring): clarify value group docstring (#16272) The "value group" of a valuation is not a group! It's a group with zero. I've heard the phrase "value group" being used to describe the units of this group with zero before, so we should perhaps clarify in the docstring what we mean by this definition.