Real.abs

Stream: Is there code for X?

[Kevin Buzzard]

import Mathlib

-- this exists
#check (Complex.abs : AbsoluteValue ℂ ℝ)

-- Do we have a name for this?
#check (IsAbsoluteValue.toAbsoluteValue (norm : ℝ → ℝ) : AbsoluteValue ℝ ℝ)

Should this be called Real.abs? It shows up in #16483 .

[Daniel Weber]

Isn't this just docs#AbsoluteValue.abs ?

[Michael Stoll]

The reason there is a special one for the complex numbers is that it is real-valued and not complex-valued.