mathlib

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

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 𝕂 𝕂']`.