[Merged by Bors] - refactor(algebra/abs): add has_abs class

[mans0954]

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 #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:

mathlib/src/algebra/ordered_group.lean

Line 984 in f36c98e

def abs {α : Type*} [has_neg α] [linear_order α] (a : α) : α := max a (-a)

mathlib/src/topology/continuous_function/basic.lean

Line 113 in f36c98e

def abs (f : C(α, β)) : C(α, β) :=

Out of scope are the following abs : α → β:

mathlib/src/data/complex/is_R_or_C.lean

Line 439 in f36c98e

@[pp_nodot] noncomputable def abs (z : K) : ℝ := (norm_sq z).sqrt

mathlib/src/data/complex/basic.lean

Line 406 in f36c98e

@[pp_nodot] noncomputable def abs (z : ℂ) : ℝ := (norm_sq z).sqrt

mathlib/src/data/real/nnreal.lean

Line 762 in f36c98e

@[pp_nodot] def real.nnabs (x : ℝ) : ℝ≥0 := ⟨abs x, abs_nonneg x⟩

mathlib/src/data/num/basic.lean

Line 315 in f36c98e

def abs : znum → num

Replacing the abs notation with |.| can be considered in a subsequent PR.

---

[semorrison]

(Incidentally, once people have started reviewing a PR, could you please avoid using force push? Reviewers often have local copies of the branch. The history gets squashed anyway when we merge to master, so it doesn't matter if it is messy during the PR process.)

[jcommelin]

Thanks 🎉

bors merge

[bors]

Build failed (retrying...):

• Build mathlib

[bors]

Build failed (retrying...):

• Build mathlib

[bors]

Build failed (retrying...):

• Build mathlib

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests