Commit 2021-08-27 12:25 023a816d

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".