Commit 2023-11-17 14:37 e4e3f2f5

View on Github →

chore: exp -> NormedSpace.exp (#8436) Per discussion at zulip

Estimated changes

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