Commit 2022-04-21 12:09 e5f82363

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.