# Zulip Chat Archive

## Stream: general

### Topic: Overloaded abs causing issues

#### Keefer Rowan (May 28 2020 at 14:32):

I think overloading abs for ordered group and complex numbers is causing issues. Here's an example:

```
import data.complex.basic
open complex
example (a : ℂ) : a.abs = abs (a.re) := sorry
```

It throws:

```
ambiguous overload, possible interpretations
abs a.re
↑(a.re).abs
Additional information:
c:\Users\keefe\OneDrive\Documents\Lean\mathlib\src\test.lean:4:26: context: switched to basic overload resolution where arguments are elaborated without any information about the expected type because it failed to disambiguate overload using the expected type
ℝ
the following overloaded terms were applicable
abs
abs
```

I'm not sure how to deal with this, as writing `example (a : ℂ) : a.abs = abs (a.re : ℝ) := sorry`

doesn't help. My best guess is it has to do type class inference for `ordered_group`

and for coercion to $\mathbb{C}$ and they have the same priority, or something like that. I don't know how to work around (a suggestion on that would be helpful), but it also seems like this is a problem worth fixing in mathlib too. Perhaps renaming complex abs, making it protected, or changing priorities? Since complex abs is a norm, it seems like we should make it protected and then canonically use the norm notation outside of the `basic`

file. Thoughts?

#### Reid Barton (May 28 2020 at 14:34):

Not an expert on this part of mathlib, but all your suggestions sound reasonable. As a local workaround, you can use `open complex (hiding abs)`

which would simulate it being `protected`

.

#### Reid Barton (May 28 2020 at 14:35):

Oh, I overlooked "renaming complex abs"--I don't think that one sounds reasonable :upside_down:

Since dot notation `a.abs`

unambiguously gives you `complex.abs`

, making it protected should be pretty much strictly better.

#### Keefer Rowan (May 28 2020 at 14:35):

Ok, didn't know that dot notation works for protected so figured protecting was on equal footing with renaming. That's good to know!

#### Patrick Massot (May 28 2020 at 14:41):

The current mathlib handling of abs and norm is not optimal. We should probably study what the mathcomp people did. They explain it in https://hal.inria.fr/hal-02463336

#### Yury G. Kudryashov (May 29 2020 at 00:15):

Do we need `complex.abs`

Why not use `has_norm`

?

Last updated: Dec 20 2023 at 11:08 UTC