Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-11-17 14:37
e4e3f2f5
View on Github →
chore: exp -> NormedSpace.exp (
#8436
) Per discussion at
zulip
Estimated changes
Modified
Mathlib/Analysis/NormedSpace/DualNumber.lean
Modified
Mathlib/Analysis/NormedSpace/Exponential.lean
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.algebraMap_exp_comm
added
theorem
NormedSpace.algebraMap_exp_comm_of_mem_ball
added
theorem
NormedSpace.analyticAt_exp_of_mem_ball
added
theorem
NormedSpace.continuousOn_exp
added
def
NormedSpace.expSeries
added
theorem
NormedSpace.expSeries_apply_eq'
added
theorem
NormedSpace.expSeries_apply_eq
added
theorem
NormedSpace.expSeries_apply_eq_div'
added
theorem
NormedSpace.expSeries_apply_eq_div
added
theorem
NormedSpace.expSeries_apply_zero
added
theorem
NormedSpace.expSeries_div_hasSum_exp
added
theorem
NormedSpace.expSeries_div_hasSum_exp_of_mem_ball
added
theorem
NormedSpace.expSeries_div_summable
added
theorem
NormedSpace.expSeries_div_summable_of_mem_ball
added
theorem
NormedSpace.expSeries_eq_expSeries
added
theorem
NormedSpace.expSeries_hasSum_exp
added
theorem
NormedSpace.expSeries_hasSum_exp_of_mem_ball'
added
theorem
NormedSpace.expSeries_hasSum_exp_of_mem_ball
added
theorem
NormedSpace.expSeries_radius_eq_top
added
theorem
NormedSpace.expSeries_radius_pos
added
theorem
NormedSpace.expSeries_sum_eq
added
theorem
NormedSpace.expSeries_sum_eq_div
added
theorem
NormedSpace.expSeries_summable'
added
theorem
NormedSpace.expSeries_summable
added
theorem
NormedSpace.expSeries_summable_of_mem_ball'
added
theorem
NormedSpace.expSeries_summable_of_mem_ball
added
theorem
NormedSpace.exp_add
added
theorem
NormedSpace.exp_add_of_commute
added
theorem
NormedSpace.exp_add_of_commute_of_mem_ball
added
theorem
NormedSpace.exp_add_of_mem_ball
added
theorem
NormedSpace.exp_analytic
added
theorem
NormedSpace.exp_conj'
added
theorem
NormedSpace.exp_conj
added
theorem
NormedSpace.exp_continuous
added
theorem
NormedSpace.exp_eq_exp
added
theorem
NormedSpace.exp_eq_tsum
added
theorem
NormedSpace.exp_eq_tsum_div
added
theorem
NormedSpace.exp_hasFPowerSeriesAt_zero
added
theorem
NormedSpace.exp_hasFPowerSeriesOnBall
added
theorem
NormedSpace.exp_mem_unitary_of_mem_skewAdjoint
added
theorem
NormedSpace.exp_neg
added
theorem
NormedSpace.exp_neg_of_mem_ball
added
theorem
NormedSpace.exp_nsmul
added
theorem
NormedSpace.exp_op
added
theorem
NormedSpace.exp_series_hasSum_exp'
added
theorem
NormedSpace.exp_smul
added
theorem
NormedSpace.exp_sum
added
theorem
NormedSpace.exp_sum_of_commute
added
theorem
NormedSpace.exp_units_conj'
added
theorem
NormedSpace.exp_units_conj
added
theorem
NormedSpace.exp_unop
added
theorem
NormedSpace.exp_zero
added
theorem
NormedSpace.exp_zsmul
added
theorem
NormedSpace.exp_ℝ_ℂ_eq_exp_ℂ_ℂ
added
theorem
NormedSpace.hasFPowerSeriesAt_exp_zero_of_radius_pos
added
theorem
NormedSpace.hasFPowerSeriesOnBall_exp_of_radius_pos
added
theorem
NormedSpace.invOf_exp
added
theorem
NormedSpace.invOf_exp_of_mem_ball
added
theorem
NormedSpace.isUnit_exp
added
theorem
NormedSpace.isUnit_exp_of_mem_ball
added
theorem
NormedSpace.map_exp
added
theorem
NormedSpace.map_exp_of_mem_ball
added
theorem
NormedSpace.norm_expSeries_div_summable
added
theorem
NormedSpace.norm_expSeries_div_summable_of_mem_ball
added
theorem
NormedSpace.norm_expSeries_summable'
added
theorem
NormedSpace.norm_expSeries_summable
added
theorem
NormedSpace.norm_expSeries_summable_of_mem_ball'
added
theorem
NormedSpace.norm_expSeries_summable_of_mem_ball
added
theorem
NormedSpace.of_real_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
algebraMap_exp_comm_of_mem_ball
deleted
theorem
analyticAt_exp_of_mem_ball
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_hasSum_exp_of_mem_ball
deleted
theorem
expSeries_div_summable
deleted
theorem
expSeries_div_summable_of_mem_ball
deleted
theorem
expSeries_eq_expSeries
deleted
theorem
expSeries_hasSum_exp
deleted
theorem
expSeries_hasSum_exp_of_mem_ball'
deleted
theorem
expSeries_hasSum_exp_of_mem_ball
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
expSeries_summable_of_mem_ball'
deleted
theorem
expSeries_summable_of_mem_ball
deleted
theorem
exp_add
deleted
theorem
exp_add_of_commute
deleted
theorem
exp_add_of_commute_of_mem_ball
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_hasFPowerSeriesAt_zero
deleted
theorem
exp_hasFPowerSeriesOnBall
deleted
theorem
exp_mem_unitary_of_mem_skewAdjoint
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
exp_ℝ_ℂ_eq_exp_ℂ_ℂ
deleted
theorem
hasFPowerSeriesAt_exp_zero_of_radius_pos
deleted
theorem
hasFPowerSeriesOnBall_exp_of_radius_pos
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_div_summable
deleted
theorem
norm_expSeries_div_summable_of_mem_ball
deleted
theorem
norm_expSeries_summable'
deleted
theorem
norm_expSeries_summable
deleted
theorem
norm_expSeries_summable_of_mem_ball'
deleted
theorem
norm_expSeries_summable_of_mem_ball
deleted
theorem
of_real_exp_ℝ_ℝ
deleted
theorem
star_exp
Modified
Mathlib/Analysis/NormedSpace/MatrixExponential.lean
Modified
Mathlib/Analysis/NormedSpace/QuaternionExponential.lean
Modified
Mathlib/Analysis/NormedSpace/Spectrum.lean
Modified
Mathlib/Analysis/NormedSpace/Star/Exponential.lean
Modified
Mathlib/Analysis/NormedSpace/Star/Spectrum.lean
Modified
Mathlib/Analysis/NormedSpace/TrivSqZeroExt.lean
Modified
Mathlib/Analysis/SpecialFunctions/Exponential.lean
modified
theorem
Complex.exp_eq_exp_ℂ
modified
theorem
Real.exp_eq_exp_ℝ
Modified
Mathlib/Analysis/SpecialFunctions/Trigonometric/Series.lean
Modified
Mathlib/Combinatorics/Derangements/Exponential.lean
Modified
docs/undergrad.yaml