mathlib3

023a816d - feat(algebra): define a bundled type of absolute values (#8881)

feat(algebra): define a bundled type of absolute values (#8881) The type `absolute_value R S` is a bundled version of the typeclass `is_absolute_value R S` defined in `data/real/cau_seq.lean` (why was it defined there?), putting both in one file `algebra/absolute_value.lean`. The lemmas from `is_abs_val` have been copied mostly literally, with weakened assumptions when possible. Maps between the bundled and unbundled versions are also available. We also define `absolute_value.abs` that represents the "standard" absolute value `abs`. The point of this PR is both to modernize absolute values into bundled structures, and to make it easier to extend absolute values to represent "absolute values respecting the Euclidean domain structure", and from there "absolute values that show the class group is finite". Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com> Co-authored-by: Vierkantor <vierkantor@vierkantor.com>