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 -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/790982e5-f813-4ddc-be7c-afbd25c1ba7b%40googlegroups.com.
