mathlib3

8829a0a2 - feat(algebra/absolute_value): generalize a few results to `linear_ordered_ring`s

feat(algebra/absolute_value): generalize a few results to `linear_ordered_ring`s The proofs were copied literally from `is_absolute_value`, which was defined on fields, but we can generalize them to rings with only a few tweaks.