Commit 2022-04-22 06:47 06a6044f

View on Github →

feat(analysis/normed_space/exponential): Weaken typeclass requirements (#13444) This allows the exponential to be defined independently of a choice of norm.

Estimated changes

Modified src/analysis/analytic/basic.lean

Modified src/analysis/calculus/formal_multilinear_series.lean

modified theorem formal_multilinear_series.remove_zero_coeff_succ

modified theorem formal_multilinear_series.remove_zero_coeff_zero

modified theorem formal_multilinear_series.remove_zero_of_pos

modified def formal_multilinear_series

Modified src/analysis/normed_space/exponential.lean

modified theorem exp_eq_tsum_field

modified theorem exp_series_apply_eq_field'

modified theorem exp_series_apply_eq_field

modified theorem exp_series_sum_eq_field

modified theorem exp_zero

Modified src/analysis/normed_space/multilinear.lean