Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-06 18:45 27e105d2

View on Github →

chore(analysis/normed_space/exponential): Make the 𝔸 argument implicit (#13986) exp 𝕂 𝔸 is now just exp 𝕂. This also renames two lemmas that refer to this argument in their name to no longer do so. In a few places we have to add type annotations where they weren't needed before, but nowhere do we need to resort to @.

Estimated changes

modified theorem commute.exp
modified theorem commute.exp_left
modified theorem commute.exp_right
modified theorem exp_add
modified theorem exp_eq_exp
modified theorem exp_eq_tsum
modified theorem exp_neg
modified theorem exp_series_has_sum_exp'
modified theorem exp_series_has_sum_exp
modified theorem exp_zero
modified theorem exp_zsmul
modified theorem exp_ℝ_ℂ_eq_exp_ℂ_ℂ
modified theorem inv_of_exp
modified theorem is_unit_exp
modified theorem map_exp
modified theorem prod.fst_exp
modified theorem prod.snd_exp
modified theorem ring.inverse_exp
added theorem complex.exp_eq_exp_ℂ
modified theorem has_deriv_at_exp
modified theorem has_strict_deriv_at_exp
added theorem real.exp_eq_exp_ℝ
deleted theorem real.exp_eq_exp_ℝ_ℝ