Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-23 20:37 26448a26

View on Github →

feat(analysis/normed_space/exponential): define exponential in a Banach algebra and prove basic results (#8576)

Estimated changes

added theorem continuous_on_exp
added theorem exp_add
added theorem exp_add_of_commute
added theorem exp_add_of_mem_ball
added theorem exp_analytic
added theorem exp_continuous
added theorem exp_eq_tsum
added theorem exp_eq_tsum_field
added def exp_series
added theorem exp_series_apply_eq'
added theorem exp_series_apply_eq
added theorem exp_series_has_sum_exp
added theorem exp_series_radius_pos
added theorem exp_series_sum_eq
added theorem exp_series_summable'
added theorem exp_series_summable
added theorem exp_zero
added theorem has_deriv_at_exp
added theorem has_deriv_at_exp_zero
added theorem has_fderiv_at_exp
added theorem has_fderiv_at_exp_zero
added theorem nat.cast_add_choose
modified theorem nat.cast_choose
added theorem summable.congr
added theorem summable_congr