Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-12 18:28 116ac710

View on Github →

feat(analysis/normed_space/exponential): exponentials of negations, scalar actions, and sums (#13036) The new lemmas are:

  • exp_invertible_of_mem_ball
  • exp_invertible
  • is_unit_exp_of_mem_ball
  • is_unit_exp
  • ring.inverse_exp
  • exp_neg_of_mem_ball
  • exp_neg
  • exp_sum_of_commute
  • exp_sum
  • exp_nsmul
  • exp_zsmul I don't know enough about the radius of convergence of exp to know if exp_nsmul holds more generally under extra conditions.

Estimated changes

added theorem edist_add_left
added theorem edist_add_right
added theorem edist_neg_neg
added theorem edist_sub_left
added theorem edist_sub_right
added theorem commute.exp
modified theorem exp_add_of_commute
added theorem exp_neg
added theorem exp_neg_of_mem_ball
added theorem exp_nsmul
added theorem exp_sum
added theorem exp_sum_of_commute
modified theorem exp_zero
added theorem exp_zsmul
added theorem inv_of_exp
added theorem inv_of_exp_of_mem_ball
added theorem is_unit_exp
added theorem ring.inverse_exp