Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-05 13:11 420fabf7

View on Github →

chore(analysis/normed_space/exponential): replace 1/x with x⁻¹ (#13971) Note that one_div makes ⁻¹ the simp-normal form.

Estimated changes

modified theorem exp_eq_tsum
modified theorem exp_series_apply_eq
modified theorem exp_series_has_sum_exp'
modified theorem exp_series_sum_eq
modified theorem exp_series_summable'
modified theorem norm_exp_series_summable'