mathlib3

116ac710 - feat(analysis/normed_space/exponential): exponentials of negations, scalar actions, and sums (#13036)

feat(analysis/normed_space/exponential): exponentials of negations, scalar actions, and sums (#13036) The new lemmas are: * `exp_invertible_of_mem_ball` * `exp_invertible` * `is_unit_exp_of_mem_ball` * `is_unit_exp` * `ring.inverse_exp` * `exp_neg_of_mem_ball` * `exp_neg` * `exp_sum_of_commute` * `exp_sum` * `exp_nsmul` * `exp_zsmul` I don't know enough about the radius of convergence of `exp` to know if `exp_nsmul` holds more generally under extra conditions.