mathlib3

e5f82363 - feat(analysis/normed_space/exponential): ring homomorphisms are preserved by the exponential (#13402)

feat(analysis/normed_space/exponential): ring homomorphisms are preserved by the exponential (#13402) The new results here are: * `prod.fst_exp` * `prod.snd_exp` * `exp_units_conj` * `exp_conj` * `map_exp` * `map_exp_of_mem_ball` This last lemma does all the heavy lifting, and also lets us golf `algebra_map_exp_comm`. This doesn't bother to duplicate the rest of these lemmas for the `*_of_mem_ball` version, since the proofs are trivial and those lemmas probably wouldn't be used. This also generalizes some of the lemmas about infinite sums to work with `add_monoid_hom_class`.