mathlib

c2e6e62a - feat(algebra/absolute_value): generalize a few results to `linear_ordered_ring`s (#9026)

feat(algebra/absolute_value): generalize a few results to `linear_ordered_ring`s (#9026) 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.