Commit 2021-09-30 13:44 3daae2ca

refactor(algebra/abs): add has_abs class (#9172) 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 https://github.com/leanprover-community/mathlib/pull/8673 for lattice ordered groups, along with the notation |.| and was asked by @eric-wieser and @jcommelin to add it in a separate PR and retro fit has_abs and the notation to mathlib. I tried to introduce both the has_abs class and the |.| notation in #8891 . However, I'm finding such a large and wide-ranging PR unwieldy to work with, so I'm now opening this PR which just replaces the previous definitions of abs : α → α in the following locations: https://github.com/leanprover-community/mathlib/blob/f36c98e877dd86af12606abbba5275513baa8a26/src/algebra/ordered_group.lean#L984 https://github.com/leanprover-community/mathlib/blob/f36c98e877dd86af12606abbba5275513baa8a26/src/topology/continuous_function/basic.lean#L113 Out of scope are the following abs : α → β: https://github.com/leanprover-community/mathlib/blob/f36c98e877dd86af12606abbba5275513baa8a26/src/data/complex/is_R_or_C.lean#L439 https://github.com/leanprover-community/mathlib/blob/f36c98e877dd86af12606abbba5275513baa8a26/src/data/complex/basic.lean#L406 https://github.com/leanprover-community/mathlib/blob/f36c98e877dd86af12606abbba5275513baa8a26/src/data/real/nnreal.lean#L762 https://github.com/leanprover-community/mathlib/blob/f36c98e877dd86af12606abbba5275513baa8a26/src/data/num/basic.lean#L315 Replacing the abs notation with |.| can be considered in a subsequent PR.