refactor(*): replace `abs` with vertical bar notation (#8891)
The notion of an "absolute value" occurs both in algebra (e.g. lattice ordered groups) and analysis (e.g. GM and GL-spaces). I introduced a `has_abs` notation class in #9172, along with the conventional mathematical vertical bar notation `|.|` for `abs`.
The notation vertical bar notation was already in use in some files as a local notation. This PR replaces `abs` with the vertical bar notation throughout mathlib.
