Labels associated with exponentiation, exponential and power functions (was: Help with beginning to contribute to set.mm)

[Benoit]

Continuing the discussion with Thierry and David:

I would still use "exp" for theorems related to the exponential and "pow" for theorems related to power functions.  With "itg" for theorems related to integrals, this would give "itgpow" for Jon's current "itexp".  I would also add these three lines to the table at "conventions".  The main reason is that "exp" is much more memorable than "ef"; this is more important to me than strict consistency with the labels used for the definitions.

If consistency with the definition labels has to be kept, and probably it should, then I would use "df-expt" for exponentiation (currently "df-exp") and "df-exp" for the exponential (currently "df-ef").  Overall, the complex exponential is a more important object than exponentiation as defined in set.mm (i.e. the function defined on \C \times \Z).

Benoit

[David A. Wheeler]

We are not *always* consistent with the definitions,
but I think I think we should be "mostly consistent",
have a reason to be inconsistent, and then *document* that
inconsistency (e.g., in the small table). The consistency greatly eases searching,
which is becoming more & more important over time now that
we have so many proven theorems (a good problem to have!).

We could change the labels to match the definitions, *or* we
could change the definition names to match the preferred labels.

The new proposed definition names make sense to me, and if
they help others then great!

--- David A. Wheeler