mathlib3

31b18ef9 - doc(ring_theory/valuation/valuation_ring): Value "group" is a group with zero (#17210)

doc(ring_theory/valuation/valuation_ring): Value "group" is a group with zero (#17210) I trust that Adam is using the correct naming conventions to be found in the literature, but I think it's worth clarifying that `valuation_ring.value_group` is not actually a group, it's a group with zero. See the `valuation_ring.value_group.linear_ordered_comm_group_with_zero` at https://github.com/leanprover-community/mathlib/blob/3248c5207364d38c1e2e6a29588ffd77b1906710/src/ring_theory/valuation/valuation_ring.lean#L120