Commit 2021-10-17 18:13 084702d0

chore(analysis/normed_algebra/exponential): golf, generalize (#9740)

• move real.summable_pow_div_factorial to analysis.specific_limits, golf the proof;
• use recently added lemma inv_nat_cast_smul_eq to golf the proof of equality of exponentials defined using different fields and generalize the statement: we no longer require one field to be a normed algebra over another.
• rename exp_eq_exp_of_field_extension → exp_eq_exp and exp_series_eq_exp_series_of_field_extension → exp_series_eq_exp_series because we no longer require [normed_algebra 𝕂 𝕂'].