duplicate notation cexp

Stream: mathlib4

[Floris van Doorn]

We have the following line twice in mathlib:

notation "cexp" => Complex.exp

This means that any file importing both cannot use this notation anymore, since it is now "ambiguous".

We should adopt a rule that global notation is not allowed except for the file where the definition is defined (e.g. the notation cexp is only allowed to be declared in the file defining Complex.exp).

[Kevin Buzzard]

What if we need global notation for things introduced in core, like Nat?

[Floris van Doorn]

That can be an exception, but they should be declared in a low-level file (like Init)

[Floris van Doorn]

#7297

[David Loeffler]

FWIW, I think it was probably me who introduced this – sorry!

[Eric Wieser]

Ideally we'll eventually be able to eliminate both notations in favor of docs#exp...

[Anatole Dedecker]

I think there was some pushback on that, because docs#exp is a significantly heavier import

[David Loeffler]

The context where this came up was in some argument about Gamma functions where I needed to write down a bunch of integral computations involving both Real.exp and Complex.exp in the same formulae, eventually linking them together using docs#Complex.abs_exp. So I don't think quoting general results about exponential series for Banach algebras is going to help much there.

[Eric Wieser]

The point is not using general results, but using one definition so that we don't have to use a different notation for each exp

[Eric Wieser]

Anatole Dedecker said:

I think there was some pushback on that, because docs#exp is a significantly heavier import

I think the fact the signature is exp K (x : A) for some field K currently makes it undesirable