Commit 2023-06-02 10:22 45733ccd

View on Github →

feat: port Analysis.NormedSpace.Exponential (#4567)

Estimated changes

added theorem Commute.exp
added theorem Commute.exp_left
added theorem Commute.exp_right
added theorem Function.update_exp
added theorem IsSelfAdjoint.exp
added theorem Pi.exp_apply
added theorem Pi.exp_def
added theorem Prod.fst_exp
added theorem Prod.snd_exp
added theorem Ring.inverse_exp
added theorem algebraMap_exp_comm
added theorem continuousOn_exp
added def expSeries
added theorem expSeries_apply_eq'
added theorem expSeries_apply_eq
added theorem expSeries_apply_eq_div
added theorem expSeries_apply_zero
added theorem expSeries_div_summable
added theorem expSeries_eq_expSeries
added theorem expSeries_hasSum_exp
added theorem expSeries_radius_pos
added theorem expSeries_sum_eq
added theorem expSeries_sum_eq_div
added theorem expSeries_summable'
added theorem expSeries_summable
added theorem exp_add
added theorem exp_add_of_commute
added theorem exp_add_of_mem_ball
added theorem exp_analytic
added theorem exp_conj'
added theorem exp_conj
added theorem exp_continuous
added theorem exp_eq_exp
added theorem exp_eq_tsum
added theorem exp_eq_tsum_div
added theorem exp_neg
added theorem exp_neg_of_mem_ball
added theorem exp_nsmul
added theorem exp_op
added theorem exp_series_hasSum_exp'
added theorem exp_smul
added theorem exp_sum
added theorem exp_sum_of_commute
added theorem exp_units_conj'
added theorem exp_units_conj
added theorem exp_unop
added theorem exp_zero
added theorem exp_zsmul
added theorem invOf_exp
added theorem invOf_exp_of_mem_ball
added theorem isUnit_exp
added theorem isUnit_exp_of_mem_ball
added theorem map_exp
added theorem map_exp_of_mem_ball
added theorem of_real_exp_ℝ_ℝ
added theorem star_exp